--- 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;
--- a/src/Pure/variable.ML Wed Sep 18 22:46:01 2019 +0200
+++ b/src/Pure/variable.ML Thu Sep 19 10:52:18 2019 +0200
@@ -58,6 +58,7 @@
val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
+ val add_fixes_implicit: term -> Proof.context -> Proof.context
val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
val gen_all: Proof.context -> thm -> thm
@@ -475,6 +476,9 @@
|> (snd o add_fixes xs)
|> restore_body ctxt;
+fun add_fixes_implicit t ctxt = ctxt
+ |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []));
+
(* dummy patterns *)