Removed call to obsolete totalCPUTimer function
authorpaulson
Mon, 14 Oct 1996 11:08:54 +0200
changeset 2093 8e3e56fecfbe
parent 2092 69bd90345078
child 2094 2061df98aab5
Removed call to obsolete totalCPUTimer function
src/Pure/NJ1xx.ML
--- a/src/Pure/NJ1xx.ML	Fri Oct 11 10:55:03 1996 +0200
+++ b/src/Pure/NJ1xx.ML	Mon Oct 14 11:08:54 1996 +0200
@@ -59,7 +59,7 @@
 
 (*** Timing functions ***)
 
-val CPUtimer = Timer.totalCPUTimer();
+val CPUtimer = Timer.startCPUTimer();
 
 (*A conditional timing function: applies f to () and, if the flag is true,
   prints its runtime. *)