# HG changeset patch
# User blanchet
# Date 1381236813 -7200
# Node ID af65902b6e309b01f739485ba764eeb07e351b35
# Parent  5337fd7d53c9bfa3a0fa15c8e5a0827f7c57d126
further speed up duplicate elimination

diff -r 5337fd7d53c9 -r af65902b6e30 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:41:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:53:33 2013 +0200
@@ -102,6 +102,7 @@
                      body_type T = @{typ bool}
                    | _ => false)
 
+(* TODO: get rid of *)
 fun normalize_vars t =
   let
     fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
@@ -377,19 +378,13 @@
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end
 
-fun keyed_distinct key1_of key2_of ths =
+fun fact_distinct thy facts =
   fold (fn fact as (_, th) =>
-      Net.insert_term_safe (op aconv o pairself (key2_of o key1_of o prop_of o snd)) (key1_of (prop_of th), fact))
-    ths Net.empty
+      Net.insert_term_safe (Pattern.equiv thy o pairself (normalize_eq o prop_of o snd))
+        (normalize_eq (prop_of th), fact))
+    facts Net.empty
   |> Net.entries
 
-fun hashed_keyed_distinct hash_of key1_of key2_of facts =
-  let
-    val ys = map (`(hash_of o prop_of o snd)) facts
-    val sorted_ys = sort (int_ord o pairself fst) ys
-    val grouped_ys = AList.coalesce (op =) sorted_ys
-  in maps (keyed_distinct key1_of key2_of o snd) grouped_ys end
-
 fun struct_induct_rule_on th =
   case Logic.strip_horn (prop_of th) of
     (prems, @{const Trueprop}
@@ -534,6 +529,7 @@
     []
   else
     let
+      val thy = Proof_Context.theory_of ctxt
       val chained =
         chained
         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
@@ -545,7 +541,7 @@
          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
            all_facts ctxt false ho_atp reserved add chained css
            |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
-           |> hashed_keyed_distinct size_of_term normalize_eq normalize_vars
+           |> fact_distinct thy
          end)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end