careful export of type-dependent functions, without losing their special status;

clarified modules;

--HG--
rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML
rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala

more direct balanced version Ord_List.unions;

tune Par_Exn.make: balance merge;
clarified Par_Exn.dest: later exceptions first;

follow updates of Isabelle/Pure;

disentangled nested ML files;

more trimming;

recovered some ML toplevel pp;

some trimming;

prefix of Pure/ROOT.ML required for concurrency within the ML runtime;