src/HOL/BNF/Tools/bnf_lfp.ML

         rev (Term.add_tfrees goal []))
       end;
 
     val timer = time (timer "induction");
 
-    fun mk_ctor_map_DEADID_thm ctor_inject =
-      trans OF [id_apply, iffD2 OF [ctor_inject, id_apply RS sym]];
+    fun mk_ctor_map_DEADID_thm ctor_inject map_id =
+      trans OF [id_apply, iffD2 OF [ctor_inject, map_id RS sym]];
 
     fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
 
     val IphiTs = map2 mk_pred2T passiveAs passiveBs;

       |> mk_Frees "R" IphiTs
       ||>> mk_Frees "IR" activeIphiTs;
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
     (*register new datatypes as BNFs*)
-    val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
+    val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
       if m = 0 then
-        (replicate n DEADID_bnf, map mk_ctor_map_DEADID_thm ctor_inject_thms, replicate n [],
-        map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
+        (timer, replicate n DEADID_bnf, map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's,
+        replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val f1Ts = map2 (curry op -->) passiveAs passiveYs;
         val f2Ts = map2 (curry op -->) passiveBs passiveYs;
         val p1Ts = map2 (curry op -->) passiveXs passiveAs;

           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        timer; (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
+        (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
           lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
       end;
 
       val Irel_induct_thm =
         let

         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
+    timer;
     ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs,
       co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
       ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
       set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms,
       co_rec_thms = ctor_rec_thms},