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

diff -r 51fda1c8fa2d -r 204f749f35a9 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 02 21:42:31 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 02 22:02:11 2009 +0200
@@ -450,14 +450,15 @@
   Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
 
 fun string_of_prfs full state arg =
-  Pretty.string_of (case arg of
+  Pretty.string_of
+    (case arg of
       NONE =>
         let
-          val (ctxt, (_, thm)) = Proof.get_goal state;
+          val (ctxt, thm) = Proof.flat_goal state;
           val thy = ProofContext.theory_of ctxt;
           val prf = Thm.proof_of thm;
           val prop = Thm.full_prop_of thm;
-          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
+          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
         in
           ProofSyntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
diff -r 51fda1c8fa2d -r 204f749f35a9 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Oct 02 21:42:31 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Oct 02 22:02:11 2009 +0200
@@ -434,7 +434,7 @@
     let
       val proof_state = Toplevel.enter_proof_body state;
       val ctxt = Proof.context_of proof_state;
-      val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
+      val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
     in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 local
diff -r 51fda1c8fa2d -r 204f749f35a9 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Oct 02 21:42:31 2009 +0200
+++ b/src/Tools/quickcheck.ML	Fri Oct 02 22:02:11 2009 +0200
@@ -143,7 +143,7 @@
     val thy = Proof.theory_of state;
     fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
       | strip t = t;
-    val (_, (_, st)) = Proof.get_goal state;
+    val (_, st) = Proof.flat_goal state;
     val (gi, frees) = Logic.goal_params (prop_of st) i;
     val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
       |> monomorphic_term thy insts default_T