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