src/HOL/BNF/Tools/bnf_lfp_compat.ML

     val infos = map mk_info (take nn_fp fp_sugars);
 
     val all_notes =
       (case lfp_sugar_thms of
         NONE => []
-      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) =>
+      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
         let
           val common_notes =
             (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
             |> filter_out (null o #2)
             |> map (fn (thmN, thms, attrs) =>