diff -r b640770117fd -r 16cf5090d3a6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 11:51:05 2015 +0200
@@ -769,7 +769,7 @@
   in
     state'
     |> assume assumptions
-    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+    |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
     |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 
@@ -935,8 +935,9 @@
       |> 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 (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
+      map_context (fold Variable.bind_term binds') #> after_local results);
   in
     goal_state
     |> map_context (init_context #> Variable.set_body true)