# HG changeset patch
# User wenzelm
# Date 902392124 -7200
# Node ID 1835a591d3a7eea7fc081ebc5bc4be365e617e02
# Parent  86d80749453f1630e96b6ec728e2eebc789d47dd
binding / skolem vars;

diff -r 86d80749453f -r 1835a591d3a7 src/Pure/Syntax/lexicon.ML
--- 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;