# HG changeset patch
# User wenzelm
# Date 1568883138 -7200
# Node ID ce1afe0f3071dfc2e11f59b8216d74c334a31292
# Parent  53fa2e4e79af7086d1b976bc8f024f30febbc37d
clarified modules;

diff -r 53fa2e4e79af -r ce1afe0f3071 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;
 
diff -r 53fa2e4e79af -r ce1afe0f3071 src/Pure/variable.ML
--- 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 *)