--- 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),