src/Pure/Syntax/type_ext.ML
changeset 7500 299949eddba8
parent 6901 5e20ddfdf3c7
child 8895 2913a54e64cf
--- 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),