src/Pure/Syntax/mixfix.ML

 (* mixfix_args *)
 
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = mfix_args sy
   | mixfix_args (Delimfix sy) = mfix_args sy
-  | mixfix_args _ = 2 		(*infix or binder*);
+  | mixfix_args (*infix or binder*) _ = 2;
 
 
 (* syn_ext_types *)
 
 fun syn_ext_types logtypes type_decls =

   ("",             "prop => asms",                  Delimfix "_"),
   ("_asms",        "[prop, asms] => asms",          Delimfix "_;/ _"),
   ("_bigimpl",     "[asms, prop] => prop",          Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
   ("_ofclass",     "[type, logic] => prop",         Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_mk_ofclass",  "_",                             NoSyn),
-  ("_mk_ofclassS", "_",                             NoSyn),
+  ("_TYPE",        "type => logic",                 Delimfix "(1TYPE/(1'(_')))"),
   ("_K",           "_",                             NoSyn),
   ("",             "id => logic",                   Delimfix "_"),
   ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_")];