src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   | normalize_eq t = t
 
-val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
+val normalize_eq_vars = normalize_eq #> normalize_vars
 
 fun if_thm_before th th' =
   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
 
 (* Hack: Conflate the facts about a class as seen from the outside with the

     SOME (pref, suf) => [s, pref ^ suf]
   | NONE => [s]
 
 fun build_name_tables name_of facts =
   let
-    fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
+    fun cons_thm (_, th) =
+      Termtab.cons_list (normalize_eq_vars (prop_of th), th)
     fun add_plain canon alias =
       Symtab.update (Thm.get_name_hint alias,
                      name_of (if_thm_before canon alias))
     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
     fun add_inclass (name, target) =

     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end
 
 fun uniquify facts =
   Termtab.fold (cons o snd)
-      (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
+      (fold (Termtab.default o `(normalize_eq_vars o prop_of o snd)) facts
             Termtab.empty) []
 
 fun struct_induct_rule_on th =
   case Logic.strip_horn (prop_of th) of
     (prems, @{const Trueprop}