# HG changeset patch
# User blanchet
# Date 1355267698 -3600
# Node ID 5d147d492792c7af7d9cb1ddf3890cdfd2aa2ce5
# Parent  d466ebc2781027c8438e5a203760ee096d140799
push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

diff -r d466ebc27810 -r 5d147d492792 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Dec 11 22:19:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 00:14:58 2012 +0100
@@ -25,6 +25,7 @@
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
+  val normalize_eq : term -> term
   val maybe_instantiate_inducts :
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
@@ -309,9 +310,20 @@
                   |> add Inductive [] I spec_intros
   end
 
+fun normalize_eq (t as @{const Trueprop}
+        $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
+    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
+    else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
+  | normalize_eq (t as @{const Trueprop} $ (@{const Not}
+        $ ((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
+
 fun uniquify xs =
   Termtab.fold (cons o snd)
-               (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
+      (fold (Termtab.default o `(normalize_eq o prop_of o snd)) xs
+            Termtab.empty) []
 
 fun struct_induct_rule_on th =
   case Logic.strip_horn (prop_of th) of
@@ -395,7 +407,7 @@
             (not (Config.get ctxt ignore_no_atp) andalso
              is_package_def name0) orelse
             exists (fn s => String.isSuffix s name0)
-                    (multi_base_blacklist ctxt ho_atp)) then
+                   (multi_base_blacklist ctxt ho_atp)) then
           I
         else
           let