--- a/src/Pure/Syntax/syn_ext.ML Wed Jun 02 22:25:57 1999 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Wed Jun 02 22:26:24 1999 +0200
@@ -7,8 +7,9 @@
signature SYN_EXT0 =
sig
+ val dddot_indexname: indexname
+ val constrainC: string
val typeT: typ
- val constrainC: string
val max_pri: int
end;
@@ -76,6 +77,10 @@
(** misc definitions **)
+val dddot_indexname = (Lexicon.binding "dddot", 0);
+val constrainC = "_constrain";
+
+
(* syntactic categories *)
val logic = "logic";
@@ -93,11 +98,6 @@
val anyT = Type (any, []);
-(* constants *)
-
-val constrainC = "_constrain";
-
-
(** datatype xprod **)