diff -r d1cb222438d8 -r b1cf26f2919b src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:03 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:04 2009 +0200
@@ -315,16 +315,16 @@
     fun get f = (these oo Option.map) f;
     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
-    val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
-      if s mem rsets then
+    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
+      if member (op =) rsets s then
         let
           val (d :: dummies') = dummies;
           val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
-        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
-          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
+        in (map (head_of o hd o rev o snd o strip_comb o fst o
+          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
         end
-      else ((recs, dummies), replicate (length rs) Extraction.nullt))
-        ((get #rec_thms dt_info, dummies), rss);
+      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
+        rss (get #rec_thms dt_info, dummies);
     val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
         (if c = Extraction.nullt then c else list_comb (c, map Var (rev
@@ -360,7 +360,7 @@
 
     (** realizer for induction rule **)
 
-    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
+    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
       SOME (fst (fst (dest_Var (head_of P)))) else NONE)
         (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));