src/Pure/Syntax/type_ext.ML
changeset 3829 d7333ef9e72c
parent 3778 b70c41bc7491
child 5690 4b056ee5435c
--- a/src/Pure/Syntax/type_ext.ML	Fri Oct 10 15:46:50 1997 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Fri Oct 10 15:47:41 1997 +0200
@@ -160,15 +160,21 @@
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
+   Mfix ("_",           longidT --> typeT,             "", [], 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 ("_",           longidT --> sortT,             "", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
    Mfix ("_",           idT --> classesT,              "", [], max_pri),
+   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
+   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 ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),