src/HOL/Tools/function_package/size.ML

 (*  Title:      HOL/Tools/function_package/size.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
+    Author:     Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen
 
 Size functions for datatypes.
 *)
 
 signature SIZE =

           (((s, Free (name, U)), U), name)
         end) |> split_list |>> split_list;
     val param_size = AList.lookup op = param_size_fs;
 
     val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
-      List.mapPartial (Option.map snd o lookup_size thy) |> flat;
+      map_filter (Option.map snd o lookup_size thy) |> flat;
     val extra_size = Option.map fst o lookup_size thy;
 
     val (((size_names, size_fns), def_names), def_names') =
       recTs1 ~~ alt_names' |>
       map (fn (T as Type (s, _), optname) =>

     (* characteristic equations for size functions *)
     fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr sorts) cargs;
         val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
-        val ts = List.mapPartial (fn (sT as (s, T), dt) =>
+        val ts = map_filter (fn (sT as (s, T), dt) =>
           Option.map (fn sz => sz $ Free sT)
             (if p dt then size_of_type size_of extra_size size_ofp T
              else NONE)) (tnames ~~ Ts ~~ cargs)
       in
         HOLogic.mk_Trueprop (HOLogic.mk_eq