# HG changeset patch
# User blanchet
# Date 1410177843 -7200
# Node ID 04faf6dc262e3ff127b06ea493c79ed65a779d52
# Parent  f5144942a83aa30a9bcc3d2f0d9424eab6be01fd
never include hidden names -- these cannot be referenced afterward

diff -r f5144942a83a -r 04faf6dc262e src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Sep 08 14:03:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Sep 08 14:04:03 2014 +0200
@@ -476,10 +476,10 @@
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
-           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
-           (Facts.is_concealed facts name0 orelse
-            Long_Name.is_hidden (Facts.intern facts name0) orelse
-            (not generous andalso is_blacklisted_or_something name0)) then
+           (Long_Name.is_hidden (Facts.intern facts name0) orelse
+            ((Facts.is_concealed facts name0 orelse
+              (not generous andalso is_blacklisted_or_something name0)) andalso
+             forall (not o member Thm.eq_thm_prop add_ths) ths)) then
           accum
         else
           let