--- 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));