src/Pure/Syntax/syn_ext.ML
changeset 6760 1c56eb841afe
parent 6322 7047300264c9
child 7472 f1208505d837
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 02 22:25:57 1999 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 02 22:26:24 1999 +0200
     1.3 @@ -7,8 +7,9 @@
     1.4  
     1.5  signature SYN_EXT0 =
     1.6  sig
     1.7 +  val dddot_indexname: indexname
     1.8 +  val constrainC: string
     1.9    val typeT: typ
    1.10 -  val constrainC: string
    1.11    val max_pri: int
    1.12  end;
    1.13  
    1.14 @@ -76,6 +77,10 @@
    1.15  
    1.16  (** misc definitions **)
    1.17  
    1.18 +val dddot_indexname = (Lexicon.binding "dddot", 0);
    1.19 +val constrainC = "_constrain";
    1.20 +
    1.21 +
    1.22  (* syntactic categories *)
    1.23  
    1.24  val logic = "logic";
    1.25 @@ -93,11 +98,6 @@
    1.26  val anyT = Type (any, []);
    1.27  
    1.28  
    1.29 -(* constants *)
    1.30 -
    1.31 -val constrainC = "_constrain";
    1.32 -
    1.33 -
    1.34  
    1.35  (** datatype xprod **)
    1.36