src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Sun Jun 07 22:04:50 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 07 23:37:32 2015 +0200
@@ -91,7 +91,7 @@
   val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (context -> 'a -> attribute) ->
-    ('b list -> context -> (term list list * (context -> context)) * context) ->
+    ('b list -> context -> (term list list * (indexname * term) list) * context) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
     ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text_range option * bool -> state -> state
@@ -916,13 +916,14 @@
     val chaining = can assert_chain state;
     val pos = Position.thread_data ();
 
-    val ((propss, after_ctxt), goal_state) =
+    val ((propss, binds), goal_state) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> open_block
       |> map_context_result (prepp raw_propp);
     val props = flat propss;
+    val goal_ctxt = context_of goal_state;
 
     val vars = implicit_vars props;
     val propss' = vars :: propss;
@@ -930,10 +931,10 @@
     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> Thm.cterm_of ctxt
-      |> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
+      |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
     val statement = ((kind, pos), propss', Thm.term_of goal);
-    val after_qed' = after_qed |>> (fn after_local =>
-      fn results => map_context after_ctxt #> after_local results);
+    val after_qed' = after_qed |>> (fn after_local => fn results =>
+      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)