Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed binding;
authorwenzelm
Sat, 04 Sep 1999 21:04:07 +0200
changeset 7472 f1208505d837
parent 7471 38823cea751f
child 7473 fd03510c6841
removed binding;
src/Pure/Syntax/lexicon.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/syn_ext.ML file | annotate | diff | comparison | revisions 
--- 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 "__";
 
--- 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";
isabelle