src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -151,7 +151,7 @@
         | _ => error ("Bad mixfix declaration for type: " ^ quote t))
       end;
 
-    val mfix = mapfilter mfix_of type_decls;
+    val mfix = List.mapPartial mfix_of type_decls;
     val xconsts = map name_of type_decls;
   in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
 
@@ -189,9 +189,9 @@
     fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)
       | binder _ = NONE;
 
-    val mfix = flat (map mfix_of const_decls);
+    val mfix = List.concat (map mfix_of const_decls);
     val xconsts = map name_of const_decls;
-    val binders = mapfilter binder const_decls;
+    val binders = List.mapPartial binder const_decls;
     val binder_trs = map SynTrans.mk_binder_tr binders;
     val binder_trs' =
       map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;