# HG changeset patch
# User wenzelm
# Date 1163539020 -3600
# Node ID 6cca4865e3881b779d9a33ea8c97c1510012ee98
# Parent  bffb2240d03f2079cf23aff357a3b96cf59ab385
removed fix_frees interface;
added auto_fixes (depends on body mode);

diff -r bffb2240d03f -r 6cca4865e388 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 =