diff -r b5e7b80caa6a -r a713ae348e8a src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Fri Nov 10 07:44:47 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Fri Nov 10 10:42:25 2006 +0100
@@ -248,9 +248,9 @@
                  SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
                Suc_if_eq')) (Thm.forall_intr cv' th)
       in
-        case List.mapPartial (fn th'' =>
+        case map_filter (fn th'' =>
             SOME (th'', singleton
-              (Variable.trade (Variable.thm_context th'') (fn [th'''] => [th''' RS th'])) th'')
+              (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'')
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>
@@ -309,7 +309,7 @@
   in
     if forall (can (dest o concl_of)) ths andalso
       exists (fn th => member (op =) (foldr add_term_consts
-        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) "Suc") ths
+        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
     then remove_suc_clause thy ths else ths
   end;