# HG changeset patch
# User wenzelm
# Date 928355184 -7200
# Node ID 1c56eb841afe22a0ae11ca234967900efc8d026f
# Parent  8ce58492bf50c3c7a481a259a27089db79ae0a63
added dddot_indexname;

diff -r 8ce58492bf50 -r 1c56eb841afe src/Pure/Syntax/syn_ext.ML
--- 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 **)