removed fix_frees interface;
authorwenzelm
Tue, 14 Nov 2006 22:17:00 +0100
changeset 21369 6cca4865e388
parent 21368 bffb2240d03f
child 21370 d9dd7b4e5e69
removed fix_frees interface; added auto_fixes (depends on body mode);
src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Nov 14 22:16:59 2006 +0100
+++ b/src/Pure/variable.ML	Tue Nov 14 22:17:00 2006 +0100
@@ -32,7 +32,7 @@
   val expand_binds: Proof.context -> term -> term
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
-  val fix_frees: term -> Proof.context -> Proof.context
+  val auto_fixes: term -> Proof.context -> Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val export_inst: Proof.context -> Proof.context -> string list * string list
@@ -295,7 +295,10 @@
 fun fix_frees t ctxt = ctxt
   |> add_fixes_direct
       (rev (fold_aterms (fn Free (x, _) =>
-        if is_fixed ctxt x then I else insert (op =) x | _ => I) t []))
+        if is_fixed ctxt x then I else insert (op =) x | _ => I) t []));
+
+fun auto_fixes t ctxt =
+  (if is_body ctxt then ctxt else fix_frees t ctxt)
   |> declare_term t;
 
 fun invent_types Ss ctxt =