# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID d2f21e305d0cd21e391b7dc91cf22b9c2f3ab631
# Parent  2eaaca796234b5bb0850f0bb2601252d0658bf46
stronger fact normalization

diff -r 2eaaca796234 -r d2f21e305d0c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -357,7 +357,7 @@
     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'
@@ -372,7 +372,8 @@
 
 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))
@@ -386,7 +387,7 @@
 
 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 =