diff -r 92586a978648 -r 2fda15dd1e0f src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Apr 15 18:43:21 1994 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Fri Apr 22 12:43:53 1994 +0200
@@ -65,7 +65,7 @@
       | sort tm = raise_term "typ_of_term: bad encoding of sort" [tm];
 
     fun typ (Free (x, _), scs) =
-          (if is_tfree x then TFree (x, []) else Type (x, []), scs)
+          (if is_tid x then TFree (x, []) else Type (x, []), scs)
       | typ (Var (xi, _), scs) = (TVar (xi, []), scs)
       | typ (Const ("_ofsort", _) $ Free (x, _) $ st, scs) =
           (TFree (x, []), put_sort scs (x, ~1) (sort st))
@@ -170,19 +170,19 @@
 val typesT = Type ("types", []);
 
 val type_ext = syn_ext
-  [logic, "type"]
-  [Mfix ("_",           tfreeT --> typeT,              "", [], max_pri),
+  [logic, "type"] [logic, "type"]
+  [Mfix ("_",           tidT --> typeT,              "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
-   Mfix ("_::_",        [tfreeT, sortT] ---> typeT,    "_ofsort", [max_pri, 0], max_pri),
+   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
    Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
    Mfix ("_",           idT --> classesT,              "", [], max_pri),
    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
-   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),  (* FIXME ambiguous *)
-   Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT,      "_tappl", [], max_pri),           (* FIXME ambiguous *)
+   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
+   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),