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