# HG changeset patch
# User blanchet
# Date 1504818795 -7200
# Node ID db3969568560f325cc690d7a6652127c66ac435c
# Parent  84926115c2ddf348052aeb86470180890743c133
better duplicate detection

diff -r 84926115c2dd -r db3969568560 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Sep 07 18:01:41 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Sep 07 23:13:15 2017 +0200
@@ -449,10 +449,11 @@
     val global_facts = Global_Theory.facts_of thy
     val local_facts = Proof_Context.facts_of ctxt
     val named_locals = Facts.dest_static true [global_facts] local_facts
+      |> maps (map (normalize_eq o Thm.prop_of) o snd)
   in
     fn th =>
       not (Thm.has_name_hint th) andalso
-      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
+      not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th)))
   end
 
 fun all_facts ctxt generous ho_atp keywords add_ths chained css =