--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Apr 02 20:46:44 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Apr 03 18:36:19 2015 +0200
@@ -476,7 +476,7 @@
fun add_facts global foldx facts =
foldx (fn (name0, ths) => fn accum =>
if name0 <> "" andalso
- (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse
+ (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