moved multithreaded "profile" to multithreading_polyml.ML;

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -13,6 +13,7 @@
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   val system_out: string -> string * int
   structure TimeLimit: TIME_LIMIT
+  val profile: int -> ('a -> 'b) -> 'a -> 'b
 end;
 
 signature BASIC_MULTITHREADING =
@@ -320,6 +321,16 @@
   in ! status end);
 
 
+(* profiling *)
+
+local val profile_orig = profile in
+
+fun profile 0 f x = f x
+  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
+
+end;
+
+
 (* serial numbers *)
 
 local

--- a/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -10,12 +10,3 @@
 
 val pointer_eq = PolyML.pointerEq;
 
-
-(* single-threaded profiling *)
-
-local val profile_orig = profile in
-
-fun profile 0 f x = f x
-  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
-
-end;

--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 11:52:15 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 12:14:17 2008 +0100
@@ -10,17 +10,7 @@
 val pointer_eq = PolyML.pointerEq;
 
 
-(* single-threaded profiling *)
-
-local val profile_orig = profile in
-
-fun profile 0 f x = f x
-  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
-
-end;
-
-
-(* improved versions of use_text/file *)
+(* runtime compilation *)
 
 fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
   let