src/Tools/auto_solve.ML
changeset 33290 6dcb0a970783
parent 32966 5b21661fe618
child 33301 1fe9fc908ec3
--- a/src/Tools/auto_solve.ML	Wed Oct 28 22:01:40 2009 +0100
+++ b/src/Tools/auto_solve.ML	Wed Oct 28 22:02:53 2009 +0100
@@ -61,9 +61,9 @@
       end;
 
     fun seek_against_goal () =
-      (case try Proof.flat_goal state of
+      (case try Proof.simple_goal state of
         NONE => NONE
-      | SOME (_, st) =>
+      | SOME {goal = st, ...} =>
           let
             val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
             val rs =