diff -r c3019a66180f -r 4ca3608fdf4f src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Mon Apr 05 13:23:10 2004 +0200
@@ -57,22 +57,7 @@
 
 (** Compiler-independent timing functions **)
 
-(*Note start point for timing*)
-fun startTiming() = 
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {gc,sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  GC " ^ toString (gc2-gc) ^
-      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
-      " secs"
-      handle Time => ""
-  end;
+use "ML-Systems/cpu-timer-gc.ML"
 
 
 (* ML command execution *)