# HG changeset patch
# User wenzelm
# Date 774178628 -7200
# Node ID bbaa2a02bd82b03fe6e3a14507578f92e58ec5a4
# Parent  22325fd7234e81ccaf97a73237087cd1bc5fa0c9
changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";

diff -r 22325fd7234e -r bbaa2a02bd82 src/Pure/Syntax/mixfix.ML
--- 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)];