src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

 fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
-         induct_thm, n2m, lthy) =
+         common_induct, n2m, lthy) =
       get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
 
     val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
 
     val indices = map #fp_res_index basic_lfp_sugars;

     val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
 
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
 
-    val induct_thms = unpermute0 (conj_dests nn induct_thm);
+    val inducts = unpermute0 (conj_dests nn common_induct);
 
     val lfpTs = unpermute perm_lfpTs;
     val Cs = unpermute perm_Cs;
     val ctr_offsets = unpermute perm_ctr_offsets;
 

         ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
       {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
        nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
        ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
   in
-    ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm, induct_thms),
-     lthy)
+    ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
 type eqn_data = {

     val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
     val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
         [] => ()
       | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
 
-    val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
+    val ((n2m, rec_specs, _, common_induct, inducts), lthy) =
       rec_specs_of bs arg_Ts res_Ts frees callssss lthy0;
 
     val actual_nn = length funs_data;
 
     val ctrs = maps (map #ctr o #ctr_specs) rec_specs;

         (js, simp_thms)
       end;
 
     val notes =
       (if n2m then
-         map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names
-           (take actual_nn induct_thms)
+         map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names (take actual_nn inducts)
        else
          [])
       |> map (fn (prefix, thmN, thms, attrs) =>
         ((Binding.qualify true prefix (Binding.name thmN), attrs), [(thms, [])]));
 
     val common_name = mk_common_name fun_names;
 
     val common_notes =
-      (if n2m then [(inductN, [induct_thm], [])] else [])
+      (if n2m then [(inductN, [common_induct], [])] else [])
       |> map (fn (thmN, thms, attrs) =>
         ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
   in
     (((fun_names, defs),
       fn lthy => fn defs =>