--- a/src/Pure/Syntax/mixfix.ML Wed Jul 13 10:13:52 1994 +0200
+++ b/src/Pure/Syntax/mixfix.ML Thu Jul 14 11:37:08 1994 +0200
@@ -164,7 +164,7 @@
("", "prop => asms", Delimfix "_"),
("_asms", "[prop, asms] => asms", Delimfix "_;/ _"),
("_bigimpl", "[asms, prop] => prop", Mixfix ("((3[| _ |]) ==>/ _)", [0, 1], 1)),
- ("_insort", "[type, 'a] => prop", Delimfix "(2'(| _ :/ _ |'))"),
+ ("_ofclass", "[type, 'a] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_K", "'a", NoSyn),
("_explode", "'a", NoSyn),
("_implode", "'a", NoSyn)];