changeset 70308 | 7f568724d67e |
parent 69045 | 8c240fdeffcb |
child 70364 | b2bedb022a75 |
--- a/src/Pure/Isar/proof.ML Mon Jun 03 14:47:27 2019 +0200 +++ b/src/Pure/Isar/proof.ML Mon Jun 03 15:40:08 2019 +0200 @@ -1093,7 +1093,7 @@ val (propss, binds) = prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp; val goal_ctxt = ctxt - |> (fold o fold) Variable.auto_fixes propss + |> (fold o fold) Proof_Context.augment propss |> fold Variable.bind_term binds; fun after_qed' (result_ctxt, results) ctxt' = ctxt' |> Proof_Context.restore_naming ctxt