src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49205 674f04c737e0
parent 49185 073d7d1b7488
child 49213 975ccb0130cb
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -11,7 +11,8 @@
     1.4  sig
     1.5    val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
     1.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     1.7 -    (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
     1.8 +    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     1.9 +      thm list) * local_theory
    1.10  end;
    1.11  
    1.12  structure BNF_GFP : BNF_GFP =
    1.13 @@ -2999,8 +3000,9 @@
    1.14              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.15            bs thmss)
    1.16    in
    1.17 -    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    1.18 -      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.19 +    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, coiter_thms,
    1.20 +      corec_thms),
    1.21 +     lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.22    end;
    1.23  
    1.24  val _ =