1.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Apr 27 11:27:33 1994 +0200
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Mon May 02 12:34:56 1994 +0200
     1.3 @@ -141,9 +141,12 @@
     1.4  
     1.5  (* parse ast translations *)
     1.6  
     1.7 -fun tappl_ast_tr (*"_tapp(l)"*) [types, f] =
     1.8 -      Appl (f :: unfold_ast "_types" types)
     1.9 -  | tappl_ast_tr (*"_tapp(l)"*) asts = raise_ast "tappl_ast_tr" asts;
    1.10 +fun tapp_ast_tr (*"_tapp"*) [ty, f] = Appl [f, ty]
    1.11 +  | tapp_ast_tr (*"_tapp"*) asts = raise_ast "tapp_ast_tr" asts;
    1.12 +
    1.13 +fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
    1.14 +      Appl (f :: ty :: unfold_ast "_types" tys)
    1.15 +  | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
    1.16  
    1.17  fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
    1.18        fold_ast_p "fun" (unfold_ast "_types" dom, cod)
    1.19 @@ -154,7 +157,8 @@
    1.20  
    1.21  fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
    1.22    | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
    1.23 -  | tappl_ast_tr' (f, tys) = Appl [Constant "_tappl", fold_ast "_types" tys, f];
    1.24 +  | tappl_ast_tr' (f, ty :: tys) =
    1.25 +      Appl [Constant "_tappl", ty, fold_ast "_types" tys, f];
    1.26  
    1.27  fun fun_ast_tr' (*"fun"*) asts =
    1.28    (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
    1.29 @@ -171,7 +175,7 @@
    1.30  
    1.31  val type_ext = syn_ext
    1.32    [logic, "type"] [logic, "type"]
    1.33 -  [Mfix ("_",           tidT --> typeT,              "", [], max_pri),
    1.34 +  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    1.35     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    1.36     Mfix ("_",           idT --> typeT,                 "", [], max_pri),
    1.37     Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    1.38 @@ -188,7 +192,7 @@
    1.39     Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
    1.40     Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
    1.41    []
    1.42 -  ([("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    1.43 +  ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    1.44     [],
    1.45     [],
    1.46     [("fun", fun_ast_tr')])