diff -r ac039c4981b6 -r 3e9a68bd30a7 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 16:36:23 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Mar 30 17:03:26 2016 +0200
@@ -6,7 +6,6 @@
 
 signature SYNTAX_EXT =
 sig
-  val dddot_indexname: indexname
   datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
   datatype xsymb =
@@ -56,12 +55,6 @@
 structure Syntax_Ext: SYNTAX_EXT =
 struct
 
-
-(** misc definitions **)
-
-val dddot_indexname = ("dddot", 0);
-
-
 (** datatype xprod **)
 
 (*Delim s: delimiter s