src/Pure/Isar/proof.ML
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