tuned _dummy_ofsort syntax;
authorwenzelm
Sat May 29 15:07:42 2004 +0200 (2004-05-29)
changeset 14838b12855d44c97
parent 14837 827c68f8267c
child 14839 c994f1c57fc7
tuned _dummy_ofsort syntax;
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Sat May 29 15:07:29 2004 +0200
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Sat May 29 15:07:42 2004 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4     Mfix ("_",           longidT --> typeT,             "", [], max_pri),
     1.5     Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
     1.6     Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
     1.7 -   Mfix ("'_::_",       sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
     1.8 +   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
     1.9     Mfix ("_",           idT --> sortT,                 "", [], max_pri),
    1.10     Mfix ("_",           longidT --> sortT,             "", [], max_pri),
    1.11     Mfix ("{}",          sortT,                         "_topsort", [], max_pri),