--- 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 *)