--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 17:02:49 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 20 17:17:01 2011 +0200
@@ -414,9 +414,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