src/Pure/variable.ML

   val hidden_polymorphism: term -> typ -> (indexname * sort) list
   val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
   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
   val exportT_inst: Proof.context -> Proof.context -> string list
   val export_terms: Proof.context -> Proof.context -> term list -> term list

   |> restore_body ctxt;
 
 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 =
   let
     val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;