1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 19:57:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 20:17:03 2010 +0200
     1.3 @@ -561,13 +561,14 @@
     1.4        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
     1.5            (map (name_thms_pair_from_ref ctxt chained_ths) add @
     1.6             (if only then [] else all_name_thms_pairs ctxt chained_ths))
     1.7 +      |> make_unique
     1.8        |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
     1.9                                 not (is_dangerous_term full_types (prop_of th)))
    1.10    in
    1.11      relevance_filter ctxt relevance_threshold relevance_convergence
    1.12                       defs_relevant max_new theory_relevant relevance_override
    1.13                       axioms (concl_t :: hyp_ts)
    1.14 -    |> make_unique |> sort_wrt fst
    1.15 +    |> sort_wrt fst
    1.16    end
    1.17  
    1.18  end;