# HG changeset patch
# User wenzelm
# Date 960998446 -7200
# Node ID 64464b5f686722d3e1e04c30630c00cb91ca4a85
# Parent  b1e874e38dab5a2196d43670e7305cfd14e34d1c
tuned tappl syntax;

diff -r b1e874e38dab -r 64464b5f6867 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Jun 14 17:59:53 2000 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Jun 14 18:00:46 2000 +0200
@@ -175,8 +175,8 @@
    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
-   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
-   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
+   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
+   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),