tuned;

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

--- a/src/Pure/General/long_name.ML	Thu Apr 02 20:46:44 2015 +0200
+++ b/src/Pure/General/long_name.ML	Fri Apr 03 18:36:19 2015 +0200
@@ -9,6 +9,7 @@
   val separator: string
   val is_qualified: string -> bool
   val hidden: string -> string
+  val is_hidden: string -> bool
   val dest_hidden: string -> string option
   val localN: string
   val dest_local: string -> string option
@@ -29,8 +30,10 @@
 
 val is_qualified = exists_string (fn s => s = separator);
 
-val hidden = prefix "??.";
-val dest_hidden = try (unprefix "??.");
+val hidden_prefix = "??."
+val hidden = prefix hidden_prefix;
+val is_hidden = String.isPrefix hidden_prefix;
+val dest_hidden = try (unprefix hidden_prefix);
 
 val localN = "local";
 val dest_local = try (unprefix "local.");

--- a/src/Pure/Tools/find_theorems.ML	Thu Apr 02 20:46:44 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Apr 03 18:36:19 2015 +0200
@@ -328,7 +328,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
+val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
 val qual_ord = int_ord o apply2 Long_Name.qualification;
 val txt_ord = int_ord o apply2 size;