renamed Proof.flat_goal to Proof.simple_goal;

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

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

--- 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 =