# HG changeset patch
# User wenzelm
# Date 856773972 -3600
# Node ID d5fe793293aca2fd7cd0772fe5a681fbc7ae215e
# Parent  d73a46247a4a952f0baa7a36e04faf21ad8444a3
added "_" syntax for dummyT;

diff -r d73a46247a4a -r d5fe793293ac 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)],
    [],