clarified modules;
authorwenzelm
Thu, 19 Sep 2019 10:52:18 +0200
changeset 70923 ce1afe0f3071
parent 70922 53fa2e4e79af
child 70924 31364e70ff3e
clarified modules;
src/Pure/Isar/proof_context.ML
src/Pure/variable.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;
 
--- 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 *)