--- a/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 16:18:47 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Apr 20 16:49:52 2011 +0200
@@ -221,7 +221,7 @@
sort (mode_ord o pairself (hd o snd))
(filter_out (null o snd) (ps ~~ map
(fn Prem (us, t, is_set) => sort mode_ord
- (List.mapPartial (fn m as Mode (_, is, _) =>
+ (map_filter (fn m as Mode (_, is, _) =>
let
val (in_ts, out_ts) = get_args is 1 us;
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
@@ -288,7 +288,7 @@
fun check_modes_pred thy codegen_mode arg_vs preds modes (p, ms) =
let val SOME rs = AList.lookup (op =) preds p in
- (p, List.mapPartial (fn m as (m', _) =>
+ (p, map_filter (fn m as (m', _) =>
let val xs = map (check_mode_clause thy codegen_mode arg_vs modes m) rs in
(case find_index is_none xs of
~1 => SOME (m', exists (fn SOME b => b) xs)