src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

      fp_nesting_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
   val corec_specs_of: binding list -> typ list -> typ list -> term list ->
     (term * term list list) list list -> local_theory ->
-    (bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory
+    corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
+    * bool * local_theory
   val add_primcorecursive_cmd: primcorec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
   val add_primcorec_cmd: primcorec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->

 
     val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
           common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
 
+    val coinduct_attrs_pair = (case gfp_sugar_thms of SOME ((_, _, pair), _) => pair | NONE => []);
+
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
 
     val indices = map #fp_res_index fp_sugars;
     val perm_indices = map #fp_res_index perm_fp_sugars;
 

        fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
        fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
        ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
          corec_selss};
   in
-    ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
-      co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
-      co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
+    (map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
+     co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
+     co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
+     is_some gfp_sugar_thms, lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
 val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;

       |> map (flat o snd)
       |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
         (ctr, map (K []) sels))) basic_ctr_specss);
 
-    val ((n2m, corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms,
-          coinduct_strong_thms), lthy') =
+    val (corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms,
+         (coinduct_attrs, common_coinduct_attrs), n2m, lthy') =
       corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
     val corec_specs = take actual_nn corec_specs';
     val ctr_specss = map #ctr_specs corec_specs;
 
     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data

 
         val anonymous_notes =
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
+        val common_notes =
+          [(coinductN, if n2m then [coinduct_thm] else [], common_coinduct_attrs),
+           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coindut_attrs)]
+          |> filter_out (null o #2)
+          |> map (fn (thmN, thms, attrs) =>
+            ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
+
         val notes =
-          [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
+          [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
+           (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms,
+            coinduct_attrs),
            (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),
            (excludeN, exclude_thmss, []),
            (exhaustN, nontriv_exhaust_thmss, []),
            (selN, sel_thmss, simp_attrs),
-           (simpsN, simp_thmss, []),
-           (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms, [])]
+           (simpsN, simp_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map2 (fn fun_name => fn thms =>
                 ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
               fun_names (take actual_nn thmss))
           |> filter_out (null o fst o hd o snd);
-
-        val common_notes =
-          [(coinductN, if n2m then [coinduct_thm] else [], []),
-           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], [])]
-          |> filter_out (null o #2)
-          |> map (fn (thmN, thms, attrs) =>
-            ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
       in
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
-        |> Local_Theory.notes (anonymous_notes @ notes @ common_notes)
+        |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd
       end;
 
     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
   in