src/HOL/Codatatype/Tools/bnf_gfp.ML

 *)
 
 signature BNF_GFP =
 sig
   val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
-    (term list * term list * thm list * thm list) * local_theory
+    (term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
 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, unfs, fld_unf_thms, unf_fld_thms),
+    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations"