src/HOL/Tools/BNF/bnf_gfp_grec.ML

 
     fun flatten_tyargs Ass =
       map dest_TFree live_As
       |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass);
 
-     val ((bnf, _), (_, lthy)) =
-      bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y]
-        (map Term.dest_TFree dead_Es) T ((empty_comp_cache, empty_unfolds), lthy)
+    val ((bnf, _), (_, lthy)) =
+      bnf_of_typ false Do_Inline I flatten_tyargs [Term.dest_TFree Y] (map Term.dest_TFree dead_Es)
+        T ((empty_comp_cache, empty_unfolds), lthy)
       handle BAD_DEAD (Y, Y_backdrop) =>
         (case Y_backdrop of
           Type (bad_tc, _) =>
           let
             val T = qsoty (unfreeze_fp Y);

     dtor_unfold_unique sig_map_thm ssig_induct ssig_map_thms Oper_map_thm VLeaf_map_thm
     CLeaf_map_thm Lam_transfer flat_simps flat_transfer eval_core_simps eval_core_transfer eval_def
     cutSsig_def algLam_def corecU_def live_pre_bnf pre_bnf dead_pre_bnf fp_bnf sig_bnf ssig_bnf
     dead_ssig_bnf =
   let
-    val SOME prod_fp_sugar = fp_sugar_of ctxt @{type_name prod};
-    val prod_bnf = #fp_bnf prod_fp_sugar;
+    val SOME prod_bnf = bnf_of ctxt @{type_name prod};
 
     val f' = substT Z fpT f;
     val dead_ssig_map' = substT Z fpT dead_ssig_map;
     val extdd = Term.lambda f' (HOLogic.mk_comp (eval, dead_ssig_map' $ f'));