# HG changeset patch
# User wenzelm
# Date 1303310992 -7200
# Node ID 7691cc61720a195283b9a59ee7d9b062c741b29f
# Parent  a2a9018843aee3bd0b58a3fe28d0fcd28d5331b5
standardized some ML aliases;

diff -r a2a9018843ae -r 7691cc61720a src/HOL/Mutabelle/mutabelle.ML
--- 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;
 
diff -r a2a9018843ae -r 7691cc61720a src/HOL/Mutabelle/mutabelle_extra.ML
--- 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
diff -r a2a9018843ae -r 7691cc61720a src/HOL/Tools/inductive_codegen.ML
--- 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)