src/Pure/Isar/proof.ML
changeset 60401 16cf5090d3a6
parent 60388 0c9d2a4f589d
child 60402 2cfd1ead74c3
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Jun 08 22:04:19 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Jun 09 11:51:05 2015 +0200
     1.3 @@ -769,7 +769,7 @@
     1.4    in
     1.5      state'
     1.6      |> assume assumptions
     1.7 -    |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
     1.8 +    |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
     1.9      |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
    1.10    end;
    1.11  
    1.12 @@ -935,8 +935,9 @@
    1.13        |> Thm.cterm_of ctxt
    1.14        |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
    1.15      val statement = ((kind, pos), propss', Thm.term_of goal);
    1.16 +    val binds' = map #1 binds ~~ Variable.export_terms goal_ctxt ctxt (map #2 binds);
    1.17      val after_qed' = after_qed |>> (fn after_local => fn results =>
    1.18 -      map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
    1.19 +      map_context (fold Variable.bind_term binds') #> after_local results);
    1.20    in
    1.21      goal_state
    1.22      |> map_context (init_context #> Variable.set_body true)