# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID 9750618c32edf007871ce67fb872830fda9c81b9
# Parent  d2f21e305d0cd21e391b7dc91cf22b9c2f3ab631
faster uniquification

diff -r d2f21e305d0c -r 9750618c32ed 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
@@ -385,10 +385,17 @@
     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_vars o prop_of o snd)) facts
-            Termtab.empty) []
+fun keyed_distinct key_of xs =
+  let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
+    Termtab.fold (cons o snd) tab []
+  end
+
+fun hashed_keyed_distinct hash_of key_of xs =
+  let
+    val ys = map (`hash_of) xs
+    val sorted_ys = sort (int_ord o pairself fst) ys
+    val grouped_ys = AList.coalesce (op =) sorted_ys
+  in maps (keyed_distinct key_of o snd) grouped_ys end
 
 fun struct_induct_rule_on th =
   case Logic.strip_horn (prop_of th) of
@@ -540,7 +547,8 @@
            all_facts ctxt false ho_atp reserved add chained css
            |> filter_out (member Thm.eq_thm_prop del o snd)
            |> maybe_filter_no_atps ctxt
-           |> uniquify
+           |> hashed_keyed_distinct (size_of_term o prop_of o snd)
+                  (normalize_eq_vars o prop_of o snd)
          end)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end