diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -177,7 +177,8 @@
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
-   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
+   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
+   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
   []
   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    [],