added "_" syntax for dummyT;
authorwenzelm
Mon, 24 Feb 1997 09:46:12 +0100
changeset 2678 d5fe793293ac
parent 2677 d73a46247a4a
child 2679 3eac428cdd1b
added "_" syntax for dummyT;
src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Feb 21 16:43:04 1997 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Mon Feb 24 09:46:12 1997 +0100
@@ -181,7 +181,8 @@
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
-   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
+   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
+   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   []
   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    [],