src/Pure/Syntax/mixfix.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15751 65e4790c7914
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4          | _ => error ("Bad mixfix declaration for type: " ^ quote t))
     1.5        end;
     1.6  
     1.7 -    val mfix = mapfilter mfix_of type_decls;
     1.8 +    val mfix = List.mapPartial mfix_of type_decls;
     1.9      val xconsts = map name_of type_decls;
    1.10    in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
    1.11  
    1.12 @@ -189,9 +189,9 @@
    1.13      fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)
    1.14        | binder _ = NONE;
    1.15  
    1.16 -    val mfix = flat (map mfix_of const_decls);
    1.17 +    val mfix = List.concat (map mfix_of const_decls);
    1.18      val xconsts = map name_of const_decls;
    1.19 -    val binders = mapfilter binder const_decls;
    1.20 +    val binders = List.mapPartial binder const_decls;
    1.21      val binder_trs = map SynTrans.mk_binder_tr binders;
    1.22      val binder_trs' =
    1.23        map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;