# HG changeset patch
# User wenzelm
# Date 1427877343 -7200
# Node ID 27e4d0ab0948b301e6a5d695046f659258f05d92
# Parent  43dc3c660f410aa238315f42ff50f802da3e209d
tuned signature;

diff -r 43dc3c660f41 -r 27e4d0ab0948 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 31 23:42:57 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 01 10:35:43 2015 +0200
@@ -476,7 +476,7 @@
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
-           (Long_Name.is_hidden (Facts.intern facts name0) orelse
+           (is_some (Long_Name.dest_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
diff -r 43dc3c660f41 -r 27e4d0ab0948 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Mar 31 23:42:57 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 01 10:35:43 2015 +0200
@@ -737,8 +737,6 @@
 
 (*** Isabelle helpers ***)
 
-val local_prefix = Long_Name.localN ^ Long_Name.separator
-
 fun elided_backquote_thm threshold th =
   elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
 
@@ -748,7 +746,7 @@
   if Thm.has_name_hint th then
     let val hint = Thm.get_name_hint th in
       (* There must be a better way to detect local facts. *)
-      (case try (unprefix local_prefix) hint of
+      (case Long_Name.dest_local hint of
         SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
       | NONE => hint)
     end
diff -r 43dc3c660f41 -r 27e4d0ab0948 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Tue Mar 31 23:42:57 2015 +0200
+++ b/src/Pure/General/long_name.ML	Wed Apr 01 10:35:43 2015 +0200
@@ -9,9 +9,9 @@
   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 is_local: string -> bool
+  val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
@@ -29,11 +29,11 @@
 
 val is_qualified = exists_string (fn s => s = separator);
 
-fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??.";
+val hidden = prefix "??.";
+val dest_hidden = try (unprefix "??.");
 
 val localN = "local";
-val is_local = String.isPrefix "local.";
+val dest_local = try (unprefix "local.");
 
 val implode = space_implode separator;
 val explode = space_explode separator;
diff -r 43dc3c660f41 -r 27e4d0ab0948 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 31 23:42:57 2015 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 01 10:35:43 2015 +0200
@@ -235,7 +235,7 @@
   Completion.make (xname, pos) (fn completed =>
     let
       fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
-        (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
+        (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
           EQUAL =>
             (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
               EQUAL => string_ord (xname1, xname2)
diff -r 43dc3c660f41 -r 27e4d0ab0948 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Mar 31 23:42:57 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 01 10:35:43 2015 +0200
@@ -328,7 +328,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
+val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
 val qual_ord = int_ord o apply2 Long_Name.qualification;
 val txt_ord = int_ord o apply2 size;