diff -r 23e090051cb8 -r 299949eddba8 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Sep 07 10:40:58 1999 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Tue Sep 07 16:55:38 1999 +0200
@@ -156,7 +156,7 @@
 
 local open Lexicon SynExt in
 
-val type_ext = mk_syn_ext false []
+val type_ext = mk_syn_ext false ["dummy"]
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),