# HG changeset patch
# User blanchet
# Date 1412256291 -7200
# Node ID 1fc93ea5136b912e07fbb2aa785fb21ab32a105f
# Parent  251fc4a5170070d53f876817d68484046307f27f
eliminate duplicate hypotheses (which can arise due to (un)clausification)

diff -r 251fc4a51700 -r 1fc93ea5136b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 02 12:02:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 02 15:24:51 2014 +0200
@@ -104,8 +104,9 @@
       val norm_t = normalize role t
       val is_duplicate =
         exists (fn (prev_name, prev_role, prev_t, _, _) =>
-            member (op =) deps prev_name andalso
-            Term.aconv_untyped (normalize prev_role prev_t, norm_t))
+            (prev_role = Hypothesis andalso prev_t aconv t) orelse
+            (member (op =) deps prev_name andalso
+             Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
           res
 
       fun looks_boring () = t aconv @{prop False} orelse length deps < 2