--- a/src/Pure/Syntax/mixfix.ML Fri Oct 07 22:59:24 2005 +0200
+++ b/src/Pure/Syntax/mixfix.ML Fri Oct 07 22:59:25 2005 +0200
@@ -219,7 +219,9 @@
("", "'a => " ^ SynExt.args, Delimfix "_"),
("_args", "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
("", "id => idt", Delimfix "_"),
+ ("_idtdummy", "idt", Delimfix "'_"),
("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)),
+ ("_idtypdummy", "type => idt", Mixfix ("'_()::_", [], 0)),
("", "idt => idt", Delimfix "'(_')"),
("", "idt => idts", Delimfix "_"),
("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)),
@@ -237,7 +239,6 @@
("_ofclass", "[type, logic] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_mk_ofclass", "_", NoSyn),
("_TYPE", "type => logic", Delimfix "(1TYPE/(1'(_')))"),
- ("_K", "_", NoSyn),
("", "id => logic", Delimfix "_"),
("", "longid => logic", Delimfix "_"),
("", "var => logic", Delimfix "_"),
@@ -269,6 +270,7 @@
("_ofsort", "[tid, sort] => type", Mixfix ("_\\<Colon>_", [SynExt.max_pri, 0], SynExt.max_pri)),
("_constrain", "['a, type] => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtypdummy", "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
("==", "['a, 'a] => prop", InfixrName ("\\<equiv>", 2)),
("!!", "[idts, prop] => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),