diff -r c124445a4b61 -r e54ae15335a1 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
@@ -8,6 +8,7 @@
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
 val implode = SML90.implode;
 
 
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);