# HG changeset patch
# User wenzelm
# Date 902761262 -7200
# Node ID cfb74a99182c87628356bd36fec4b50c8675d74c
# Parent  2d1425492fb3a579986fb9c6c9e58583cfc48644
dest_binding, dest_skolem;

diff -r 2d1425492fb3 -r cfb74a99182c src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Aug 10 16:57:07 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Aug 10 17:01:02 1998 +0200
@@ -25,9 +25,9 @@
   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 =
@@ -327,11 +327,11 @@
 
 (* variable kinds *)
 
-fun binding x = x ^ "_";
-fun is_binding x = size x >= 1 andalso last_elem (explode x) = "_";
+val binding = suffix "_BIND_";
+val dest_binding = unsuffix "_BIND_";
 
-fun skolem x = x ^ "__";
-fun is_skolem x = size x >= 2 andalso drop (size x - 2, explode x) = ["_", "_"];
+val skolem = suffix "__";
+val dest_skolem = unsuffix "__";
 
 
 end;