tuned;

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 21 20:13:42 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Feb 22 14:28:05 2018 +0100
@@ -849,10 +849,9 @@
                 |> infer_instantiate' lthy (replicate live NONE @
                   [SOME (Thm.cterm_of lthy (ctorA $ y))])
                 |> unfold_thms lthy [dtor_ctor];
-
-              val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans);
             in
-              Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0
+              (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
+              |> Drule.generalize ([], [y_s])
             end;
 
         val map_thms =
@@ -926,13 +925,12 @@
               val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy
                 |> yield_singleton (mk_Frees "y") y_T
                 ||>> yield_singleton (mk_Frees "z") z_T;
-
-              val rel_ctor_thm0 = fp_rel_thm
-                |> infer_instantiate' lthy (replicate live NONE @
-                  [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
-                |> unfold_thms lthy [dtor_ctor];
             in
-              Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0
+              fp_rel_thm
+              |> infer_instantiate' lthy (replicate live NONE @
+                [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
+              |> unfold_thms lthy [dtor_ctor]
+              |> Drule.generalize ([], [y_s, z_s])
             end;
 
         val rel_inject_thms =

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Feb 21 20:13:42 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Feb 22 14:28:05 2018 +0100
@@ -158,9 +158,9 @@
     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);