src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Tue Jun 09 11:51:05 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 12:17:50 2015 +0200
@@ -910,21 +910,19 @@
 
 in
 
-fun generic_goal prep_propp kind before_qed after_qed propp state =
+fun generic_goal kind before_qed after_qed make_propp state =
   let
     val ctxt = context_of state;
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val (propss, binds) = prep_propp ctxt propp;
-    val props = flat propss;
-
-    val goal_state =
+    val ((propss, binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
-      |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds);
+      |> map_context_result make_propp;
+    val props = flat propss;
     val goal_ctxt = context_of goal_state;
 
     val vars = implicit_vars props;
@@ -935,6 +933,7 @@
       |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
+
     val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds);
     val after_qed' = after_qed |>> (fn after_local => fn results =>
       map_context (fold Variable.bind_term binds') #> after_local results);
@@ -980,14 +979,21 @@
     val ((names, attss), propp) =
       Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
 
+    fun make_propp ctxt' =
+      let
+        val (propss, binds) = prep_propp ctxt' propp;
+        val ctxt'' = ctxt'
+          |> (fold o fold) Variable.declare_term propss
+          |> Proof_Context.bind_terms binds;
+      in ((propss, binds), ctxt'') end;
+
     fun after_qed' results =
       local_results ((names ~~ attss) ~~ results)
       #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
       #> after_qed results;
   in
     state
-    |> map_context (Variable.set_body true)
-    |> generic_goal prep_propp kind before_qed (after_qed', K I) propp
+    |> generic_goal kind before_qed (after_qed', K I) make_propp
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
@@ -1003,9 +1009,16 @@
 (* global goals *)
 
 fun global_goal prep_propp before_qed after_qed propp =
-  init
-  #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) ""
-    before_qed (K I, after_qed) propp;
+  let
+    fun make_propp ctxt' =
+      let
+        val (propss, binds) =
+          prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') propp;
+        val ctxt'' = ctxt'
+          |> (fold o fold) Variable.auto_fixes propss
+          |> Proof_Context.bind_terms binds;
+      in ((propss, binds), ctxt'') end;
+  in init #> generic_goal "" before_qed (K I, after_qed) make_propp end;
 
 val theorem = global_goal Proof_Context.cert_propp;
 val theorem_cmd = global_goal Proof_Context.read_propp;