src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

   (case Thm.prop_of split of
     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
-      val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
     in
-      Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
+      Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
+      |> Drule.generalize ([], [s])
     end
   | _ => split);
 
 fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let