src/Pure/Isar/proof.ML

     val assumptions =
       asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
   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;
 
 in
 

     val goal =
       Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
       |> 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)
     |> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
     |> map_context (Proof_Context.auto_bind_goal props)