src/Pure/Syntax/lexicon.ML

   val read_var: string -> term
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
   val binding: string -> string
-  val is_binding: string -> bool
+  val dest_binding: string -> string
   val skolem: string -> string
-  val is_skolem: string -> bool
+  val dest_skolem: string -> string
 end;
 
 signature LEXICON =
 sig
   include LEXICON0

   end;
 
 
 (* variable kinds *)
 
-fun binding x = x ^ "_";
-fun is_binding x = size x >= 1 andalso last_elem (explode x) = "_";
-
-fun skolem x = x ^ "__";
-fun is_skolem x = size x >= 2 andalso drop (size x - 2, explode x) = ["_", "_"];
+val binding = suffix "_BIND_";
+val dest_binding = unsuffix "_BIND_";
+
+val skolem = suffix "__";
+val dest_skolem = unsuffix "__";
 
 
 end;