removed binding;
authorwenzelm
Sat Sep 04 21:04:07 1999 +0200 (1999-09-04)
changeset 7472f1208505d837
parent 7471 38823cea751f
child 7473 fd03510c6841
removed binding;
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Sat Sep 04 21:02:55 1999 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Sep 04 21:04:07 1999 +0200
     1.3 @@ -24,8 +24,6 @@
     1.4    val const: string -> term
     1.5    val free: string -> term
     1.6    val var: indexname -> term
     1.7 -  val binding: string -> string
     1.8 -  val dest_binding: string -> string
     1.9    val skolem: string -> string
    1.10    val dest_skolem: string -> string
    1.11    val read_nat: string -> int option
    1.12 @@ -328,9 +326,6 @@
    1.13  
    1.14  (* variable kinds *)
    1.15  
    1.16 -val binding = suffix "_BIND_";
    1.17 -val dest_binding = unsuffix "_BIND_";
    1.18 -
    1.19  val skolem = suffix "__";
    1.20  val dest_skolem = unsuffix "__";
    1.21  
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Sep 04 21:02:55 1999 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Sep 04 21:04:07 1999 +0200
     2.3 @@ -77,7 +77,7 @@
     2.4  
     2.5  (** misc definitions **)
     2.6  
     2.7 -val dddot_indexname = (Lexicon.binding "dddot", 0);
     2.8 +val dddot_indexname = ("dddot", 0);
     2.9  val constrainC = "_constrain";
    2.10  
    2.11