--- 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