# HG changeset patch
# User wenzelm
# Date 1128718765 -7200
# Node ID b6e0d8323c0ecda120c7351e3f9908059b939e12
# Parent  f06d6498ebf0eb761d2a20302a3230157a75be79
added syntax for _idtdummy, _idtypdummy;
removed obsolete _K;

diff -r f06d6498ebf0 -r b6e0d8323c0e src/Pure/Syntax/mixfix.ML
--- 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)),