added TYPE syntax;
authorwenzelm
Wed Nov 05 11:40:23 1997 +0100 (1997-11-05)
changeset 41434bd5f4c05cf6
parent 4142 d182dc0a34f6
child 4144 873489c611fc
added TYPE syntax;
tuned;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Nov 05 11:35:07 1997 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Nov 05 11:40:23 1997 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  fun mixfix_args NoSyn = 0
     1.5    | mixfix_args (Mixfix (sy, _, _)) = mfix_args sy
     1.6    | mixfix_args (Delimfix sy) = mfix_args sy
     1.7 -  | mixfix_args _ = 2 		(*infix or binder*);
     1.8 +  | mixfix_args (*infix or binder*) _ = 2;
     1.9  
    1.10  
    1.11  (* syn_ext_types *)
    1.12 @@ -189,7 +189,7 @@
    1.13    ("_bigimpl",     "[asms, prop] => prop",          Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    1.14    ("_ofclass",     "[type, logic] => prop",         Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.15    ("_mk_ofclass",  "_",                             NoSyn),
    1.16 -  ("_mk_ofclassS", "_",                             NoSyn),
    1.17 +  ("_TYPE",        "type => logic",                 Delimfix "(1TYPE/(1'(_')))"),
    1.18    ("_K",           "_",                             NoSyn),
    1.19    ("",             "id => logic",                   Delimfix "_"),
    1.20    ("",             "longid => logic",               Delimfix "_"),