# HG changeset patch
# User wenzelm
# Date 936471847 -7200
# Node ID f1208505d83779c23ed10c5c972212e0d70e6225
# Parent  38823cea751f13fee249415738cc02d8f58bc643
removed binding;

diff -r 38823cea751f -r f1208505d837 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Sep 04 21:02:55 1999 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Sep 04 21:04:07 1999 +0200
@@ -24,8 +24,6 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
-  val binding: string -> string
-  val dest_binding: string -> string
   val skolem: string -> string
   val dest_skolem: string -> string
   val read_nat: string -> int option
@@ -328,9 +326,6 @@
 
 (* variable kinds *)
 
-val binding = suffix "_BIND_";
-val dest_binding = unsuffix "_BIND_";
-
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
 
diff -r 38823cea751f -r f1208505d837 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Sat Sep 04 21:02:55 1999 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Sep 04 21:04:07 1999 +0200
@@ -77,7 +77,7 @@
 
 (** misc definitions **)
 
-val dddot_indexname = (Lexicon.binding "dddot", 0);
+val dddot_indexname = ("dddot", 0);
 val constrainC = "_constrain";