src/HOL/Codatatype/Tools/bnf_lfp.ML

 *)
 
 signature BNF_LFP =
 sig
   val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
-    term list * Proof.context
+    (term list * term list * thm list * thm list) * Proof.context
 end;
 
 structure BNF_LFP : BNF_LFP =
 struct
 

         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    (flds, lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
+    ((flds, unfs, fld_unf_thms, unf_fld_thms),
+      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations"
     (Parse.and_list1