new profiling function

--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 08 19:34:56 2004 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Jul 09 11:13:36 2004 +0200
@@ -155,3 +155,13 @@
   (case OS.Process.getEnv var of
     NONE => ""
   | SOME txt => txt);
+
+
+(* profiling: version that works even with 
+ML{*profiling 1*}
+apply \\<dots>
+ML{*profiling 0*}
+*)
+
+val profiling: int->unit =
+     RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;