# HG changeset patch
# User wenzelm
# Date 789818002 -3600
# Node ID 8d45c937a485852bac83224be036e38b38a2315e
# Parent  14b96e3bd4ab2e75e2961a324aa9883250f316ac
slightly changed OFCLASS syntax;

diff -r 14b96e3bd4ab -r 8d45c937a485 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Jan 02 12:16:12 1995 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 11 10:53:22 1995 +0100
@@ -159,7 +159,7 @@
   ("",          "prop => asms",                   Delimfix "_"),
   ("_asms",     "[prop, asms] => asms",           Delimfix "_;/ _"),
   ("_bigimpl",  "[asms, prop] => prop",           Mixfix ("((3[| _ |]) ==>/ _)", [0, 1], 1)),
-  ("_ofclass",  "[type, 'a] => prop",             Delimfix "(1OFCLASS/(1'(_,/ _')))"),
+  ("_ofclass",  "[type, logic] => prop",          Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_K",        "'a",                             NoSyn),
   ("",          "id => logic",                    Delimfix "_"),
   ("",          "var => logic",                   Delimfix "_"),