# HG changeset patch
# User wenzelm
# Date 1256763773 -3600
# Node ID 6dcb0a970783778971eeafaf57b7f8754aa43437
# Parent  d0c2ef49061392c38a591a9a2ea1a6b2ca2f742d
renamed Proof.flat_goal to Proof.simple_goal;

diff -r d0c2ef490613 -r 6dcb0a970783 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 28 22:01:40 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 28 22:02:53 2009 +0100
@@ -454,7 +454,7 @@
     (case arg of
       NONE =>
         let
-          val (ctxt, thm) = Proof.flat_goal state;
+          val {context = ctxt, goal = thm} = Proof.simple_goal state;
           val thy = ProofContext.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
diff -r d0c2ef490613 -r 6dcb0a970783 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Oct 28 22:01:40 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 28 22:02:53 2009 +0100
@@ -456,7 +456,7 @@
     let
       val proof_state = Toplevel.enter_proof_body state;
       val ctxt = Proof.context_of proof_state;
-      val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
+      val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
     in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 local
diff -r d0c2ef490613 -r 6dcb0a970783 src/Tools/auto_solve.ML
--- 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 =