--- a/src/HOL/Mutabelle/mutabelle.ML Wed Apr 20 16:18:47 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed Apr 20 16:49:52 2011 +0200
@@ -76,7 +76,7 @@
val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
val consts = Symtab.dest const_table
in
- List.mapPartial (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
+ map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
(filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
end;
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 16:18:47 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 16:49:52 2011 +0200
@@ -412,9 +412,9 @@
val mutants = mutants
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
- |> List.mapPartial (try (Sign.cert_term thy))
- |> List.filter (is_some o try (Thm.cterm_of thy))
- |> List.filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
+ |> map_filter (try (Sign.cert_term thy))
+ |> filter (is_some o try (Thm.cterm_of thy))
+ |> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
|> take_random max_mutants
val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
--- 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)