# HG changeset patch
# User wenzelm
# Date 1254513774 -7200
# Node ID a4ab5d0cccd1b6d914e57777b2ba8047d2be8214
# Parent  204f749f35a9574a9409b4ee03f99340b15f4b45
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
tuned;

diff -r 204f749f35a9 -r a4ab5d0cccd1 src/Tools/auto_solve.ML
--- 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;