# HG changeset patch
# User haftmann
# Date 1232027545 -3600
# Node ID c49b4c8f2eaabf84e92eeac80e68d2483f20d4d8
# Parent  a189c6274c7ae1d574b1dc186db0a1ca1480e1b1
tuned

diff -r a189c6274c7a -r c49b4c8f2eaa src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Thu Jan 15 14:52:24 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Thu Jan 15 14:52:25 2009 +0100
@@ -1,6 +1,5 @@
 (*  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.
 *)
@@ -81,7 +80,7 @@
     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') =
@@ -180,7 +179,7 @@
       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)