binding / skolem vars;

--- a/src/Pure/Syntax/lexicon.ML	Wed Aug 05 18:21:37 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Aug 06 10:28:44 1998 +0200
@@ -24,6 +24,10 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
+  val binding: string -> string
+  val is_binding: string -> bool
+  val skolem: string -> string
+  val is_skolem: string -> bool
 end;
 
 signature LEXICON =
@@ -321,4 +325,13 @@
   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) = ["_", "_"];
+
+
 end;