# HG changeset patch
# User wenzelm
# Date 1085836062 -7200
# Node ID b12855d44c97241f6f5ee22b028f0f457ae2a8dd
# Parent  827c68f8267ca83e514958f2f6293d1834dc7187
tuned _dummy_ofsort syntax;

diff -r 827c68f8267c -r b12855d44c97 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sat May 29 15:07:29 2004 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sat May 29 15:07:42 2004 +0200
@@ -196,7 +196,7 @@
    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
-   Mfix ("'_::_",       sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
+   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
    Mfix ("_",           longidT --> sortT,             "", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),