# HG changeset patch
# User paulson
# Date 845631158 -7200
# Node ID 5d44339454a4abd9d7908ec282c0d93a50128f24
# Parent  4a299f5408b7083ec60e4b8e9977a5d40c185833
Moving the CPUtimer declaration into cond_timeit should
prevent the problems that caused exn TIME to be raised

diff -r 4a299f5408b7 -r 5d44339454a4 src/Pure/NJ1xx.ML
--- a/src/Pure/NJ1xx.ML	Fri Oct 18 11:31:33 1996 +0200
+++ b/src/Pure/NJ1xx.ML	Fri Oct 18 11:32:38 1996 +0200
@@ -59,14 +59,13 @@
 
 (*** Timing functions ***)
 
-val CPUtimer = Timer.startCPUTimer();
-
 (*A conditional timing function: applies f to () and, if the flag is true,
   prints its runtime. *)
 fun cond_timeit flag f =
   if flag then
     let open Time  (*...for Time.toString, Time.+ and Time.- *)
-	val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
+	val CPUtimer = Timer.startCPUTimer();
+        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
         val result = f();
         val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
     in  print("User " ^ toString (usrt2-usrt1) ^