# HG changeset patch
# User paulson
# Date 845284134 -7200
# Node ID 8e3e56fecfbe30a2697b545becce7e629cd6c910
# Parent  69bd90345078e7f7486fd40fee36b40b8769b465
Removed call to obsolete totalCPUTimer function

diff -r 69bd90345078 -r 8e3e56fecfbe 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. *)