slightly changed OFCLASS syntax;
authorwenzelm
Wed, 11 Jan 1995 10:53:22 +0100
changeset 842 8d45c937a485
parent 841 14b96e3bd4ab
child 843 c1a4a4206102
slightly changed OFCLASS syntax;
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 "_"),