tuned signature;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -430,7 +430,7 @@
   | NONE => [ax])
 
 fun external_frees t =
-  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
+  [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
 
 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   if Config.get ctxt instantiate_inducts then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -144,7 +144,7 @@
         val do_preplay = preplay_timeout <> Time.zeroTime
         val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
 
-        val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+        val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
         fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
 
         fun get_role keep_role ((num, _), role, t, rule, _) =

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -427,9 +427,9 @@
 (* check Skolem constants *)
 
 fun no_skolem internal x =
-  if can Name.dest_skolem x then
+  if Name.is_skolem x then
     error ("Illegal reference to internal Skolem constant: " ^ quote x)
-  else if not internal andalso can Name.dest_internal x then
+  else if not internal andalso Name.is_internal x then
     error ("Illegal reference to internal variable: " ^ quote x)
   else x;
 
@@ -520,7 +520,7 @@
     (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Context_Position.report ctxt pos
-            (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
+            (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free));
           Free (x, infer_type ctxt (x, ty)))
     | _ => prep_const_proper ctxt strict (c, pos))
   end;
@@ -1375,7 +1375,7 @@
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
-        filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
+        filter_out ((Name.is_internal orf member (op =) structs) o #1)
           (Variable.dest_fixes ctxt);
       val prt_fixes =
         if null fixes then []

--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -51,7 +51,7 @@
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
-  [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+  [if Name.is_skolem x then Markup.skolem else Markup.free] @
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);
@@ -664,7 +664,7 @@
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
   in
-    if can Name.dest_skolem x
+    if Name.is_skolem x
     then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     else ([m, Markup.free], x)
   end;

--- a/src/Pure/Syntax/syntax_trans.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -124,7 +124,7 @@
   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
 
 fun absfree_proper (x, T) t =
-  if can Name.dest_internal x
+  if Name.is_internal x
   then error ("Illegal internal variable in abstraction: " ^ quote x)
   else absfree (x, T) t;
 
@@ -316,7 +316,7 @@
     val body = body_of tm;
     val rev_new_vars = Term.rename_wrt_term body vars;
     fun subst (x, T) b =
-      if can Name.dest_internal x andalso not (Term.is_dependent b)
+      if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
     val (rev_vars', body') = fold_map subst rev_new_vars body;

--- a/src/Pure/name.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/name.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -13,8 +13,10 @@
   val is_bound: string -> bool
   val internal: string -> string
   val dest_internal: string -> string
+  val is_internal: string -> bool
   val skolem: string -> string
   val dest_skolem: string -> string
+  val is_skolem: string -> bool
   val clean_index: string * int -> string * int
   val clean: string -> string
   type context
@@ -63,9 +65,11 @@
 
 val internal = suffix "_";
 val dest_internal = unsuffix "_";
+val is_internal = String.isSuffix "_";
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
+val is_skolem = String.isSuffix "__";
 
 fun clean_index (x, i) =
   (case try dest_internal x of

--- a/src/Pure/variable.ML	Thu Mar 06 10:11:38 2014 +0100
+++ b/src/Pure/variable.ML	Thu Mar 06 10:12:47 2014 +0100
@@ -399,7 +399,7 @@
 fun add_fixes_binding bs ctxt =
   let
     val _ =
-      (case filter (can Name.dest_skolem o Binding.name_of) bs of
+      (case filter (Name.is_skolem o Binding.name_of) bs of
         [] => ()
       | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
     val _ =
@@ -417,7 +417,7 @@
 fun variant_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;
-    val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
+    val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
     val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
   in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;