tuned names of start_timing,/end_timing/check_timer;

--- a/src/Provers/blast.ML	Fri Nov 10 22:18:54 2006 +0100
+++ b/src/Provers/blast.ML	Fri Nov 10 23:22:01 2006 +0100
@@ -902,7 +902,7 @@
 
 fun printStats (b, start, tacs) =
   if b then
-    writeln (endTiming start ^ " for search.  Closed: "
+    writeln (end_timing start ^ " for search.  Closed: "
              ^ Int.toString (!nclosed) ^
              " tried: " ^ Int.toString (!ntried) ^
              " tactics: " ^ Int.toString (length tacs))
@@ -1253,7 +1253,7 @@
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
       fun cont (tacs,_,choices) =
-          let val start = startTiming()
+          let val start = start_timing ()
           in
           case Seq.pull(EVERY' (rev tacs) i st) of
               NONE => (writeln ("PROOF FAILED for depth " ^
@@ -1262,7 +1262,7 @@
                        else ();
                        backtrack choices)
             | cell => (if (!trace orelse !stats)
-                       then writeln (endTiming start ^ " for reconstruction")
+                       then writeln (end_timing start ^ " for reconstruction")
                        else ();
                        Seq.make(fn()=> cell))
           end
@@ -1271,12 +1271,12 @@
   handle PROVE     => Seq.empty;
 
 (*Public version with fixed depth*)
-fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
+fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
 
 val depth_limit = ref 20;
 
 fun blast_tac cs i st =
-    ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i
+    ((DEEPEN (1, !depth_limit) (timing_depth_tac (start_timing ()) cs) 0) i
      THEN flexflex_tac) st
     handle TRANS s =>
       ((if !trace then warning ("blast: " ^ s) else ());
@@ -1296,7 +1296,7 @@
                                fromSubgoal (List.nth(prems_of st, i-1)))
                 val hyps  = strip_imp_prems skoprem
                 and concl = strip_imp_concl skoprem
-        in timeap prove (sign, startTiming(), cs,
+        in timeap prove (sign, start_timing (), cs,
                          [initBranch (mkGoal concl :: hyps, lim)], I)
         end
         handle Subscript => error("There is no subgoal " ^ Int.toString i);
@@ -1309,7 +1309,7 @@
 fun tryInThy thy lim s =
     (initialize thy;
      timeap prove (thy,
-                   startTiming(),
+                   start_timing(),
                    Data.claset(),
                    [initBranch ([readGoal thy s], lim)],
                    I));

--- a/src/Pure/General/output.ML	Fri Nov 10 22:18:54 2006 +0100
+++ b/src/Pure/General/output.ML	Fri Nov 10 23:22:01 2006 +0100
@@ -188,9 +188,9 @@
   prints its runtime on warning channel*)
 fun cond_timeit flag f =
   if flag then
-    let val start = startTiming()
+    let val start = start_timing ()
         val result = f ()
-    in info (endTiming start); result end
+    in info (end_timing start); result end
   else f ();
 
 (*unconditional timing function*)
@@ -230,9 +230,9 @@
     fun add_diff time time1 time2 =
       Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
     val {name, timer, sys, usr, gc, count} = time_check ti;
-    val (sys1, usr1, gc1) = checkTimer timer;
+    val (sys1, usr1, gc1) = check_timer timer;
     val result = capture f x;
-    val (sys2, usr2, gc2) = checkTimer timer;
+    val (sys2, usr2, gc2) = check_timer timer;
   in
     ti := TI
      {name = name,

--- a/src/Pure/ML-Systems/poplogml.ML	Fri Nov 10 22:18:54 2006 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Fri Nov 10 23:22:01 2006 +0100
@@ -247,9 +247,9 @@
 
 (** Compiler-independent timing functions **)
 
-fun startTiming() = "FIXME";
-fun endTiming (s: string) = s;
-fun checkTimer _ = (0, 0, 0);
+fun start_timing() = "FIXME";
+fun end_timing (s: string) = s;
+fun check_timer _ = (0, 0, 0);
 
 structure Timer =
 struct