diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -230,15 +230,15 @@
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
-fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
+fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
-    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
+    val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   in
-    induction
-    |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
-    |> RuleCases.save induction
+    induct
+    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+    |> RuleCases.save induct
   end;
 
 local