--- a/src/Tools/auto_solve.ML Fri Oct 02 22:02:11 2009 +0200
+++ b/src/Tools/auto_solve.ML Fri Oct 02 22:02:54 2009 +0200
@@ -16,7 +16,7 @@
val limit : int Unsynchronized.ref
end;
-structure AutoSolve : AUTO_SOLVE =
+structure Auto_Solve : AUTO_SOLVE =
struct
(* preferences *)
@@ -61,14 +61,14 @@
end;
fun seek_against_goal () =
- (case try Proof.get_goal state of
+ (case try Proof.flat_goal state of
NONE => NONE
- | SOME (_, (_, goal)) =>
+ | SOME (_, st) =>
let
- val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+ val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
val rs =
if length subgoals = 1
- then [(NONE, find goal)]
+ then [(NONE, find st)]
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
val results = filter_out (null o snd) rs;
in if null results then NONE else SOME results end);
@@ -87,7 +87,7 @@
Pretty.markup Markup.hilite
(separate (Pretty.brk 0) (map prt_result results))])
| _ => state)
- end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+ end handle TimeLimit.TimeOut => (warning "Auto solve: timeout"; state);
in
if int andalso ! auto andalso not (! Toplevel.quiet)
then go ()
@@ -96,6 +96,6 @@
end;
-val auto_solve = AutoSolve.auto;
-val auto_solve_time_limit = AutoSolve.auto_time_limit;
+val auto_solve = Auto_Solve.auto;
+val auto_solve_time_limit = Auto_Solve.auto_time_limit;