--- a/src/Pure/pure_thy.ML Fri Nov 24 22:05:19 2006 +0100
+++ b/src/Pure/pure_thy.ML Sun Nov 26 18:07:16 2006 +0100
@@ -569,12 +569,12 @@
("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", "[tid, sort] => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
("_constrain", "['a, type] => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtyp", "[id, type] => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", "'a", NoSyn),
("_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)),
+ ("all_binder", "[idts, prop] => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
("==>", "[prop, prop] => prop", InfixrName ("\\<Longrightarrow>", 1)),
("_DDDOT", "aprop", Delimfix "\\<dots>"),
("_bigimpl", "[asms, prop] => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),