author | paulson |
Mon, 14 Oct 1996 11:08:54 +0200 | |
changeset 2093 | 8e3e56fecfbe |
parent 2092 | 69bd90345078 |
child 2094 | 2061df98aab5 |
src/Pure/NJ1xx.ML | file | annotate | diff | comparison | revisions |
--- 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. *)