src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Wed Sep 18 22:46:01 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Sep 19 10:52:18 2019 +0200
@@ -417,8 +417,7 @@
 (* augment context by implicit term declarations *)
 
 fun augment t ctxt = ctxt
-  |> not (Variable.is_body ctxt) ?
-      Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t []))
+  |> Variable.add_fixes_implicit t
   |> Variable.declare_term t
   |> Soft_Type_System.augment t;