Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/mixfix.ML
changeset 4143 4bd5f4c05cf6
parent 4053 c88d0d5ae806
child 4697 101d384b69b2 
--- a/src/Pure/Syntax/mixfix.ML	Wed Nov 05 11:35:07 1997 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Nov 05 11:40:23 1997 +0100
@@ -88,7 +88,7 @@
 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 *)
@@ -189,7 +189,7 @@
   ("_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 "_"),
isabelle