tuned tappl syntax;
authorwenzelm
Wed Jun 14 18:00:46 2000 +0200 (2000-06-14)
changeset 906764464b5f6867
parent 9066 b1e874e38dab
child 9068 202fdf72cf23
tuned tappl syntax;
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Jun 14 17:59:53 2000 +0200
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Jun 14 18:00:46 2000 +0200
     1.3 @@ -175,8 +175,8 @@
     1.4     Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
     1.5     Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
     1.6     Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
     1.7 -   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
     1.8 -   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
     1.9 +   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
    1.10 +   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
    1.11     Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    1.12     Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    1.13     Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),