--- 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