# 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";