# 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