src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49126 1bbd7a37fc29
parent 49125 5fc5211cf104
child 49128 1a86ef0a0210
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 15:51:32 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 16:17:22 2012 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  signature BNF_GFP =
     1.5  sig
     1.6    val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
     1.7 -    (term list * term list * thm list * thm list) * local_theory
     1.8 +    (term list * term list * thm list * thm list * thm list) * local_theory
     1.9  end;
    1.10  
    1.11  structure BNF_GFP : BNF_GFP =
    1.12 @@ -2989,7 +2989,7 @@
    1.13              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.14            bs thmss)
    1.15    in
    1.16 -    ((flds, unfs, fld_unf_thms, unf_fld_thms),
    1.17 +    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    1.18        lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.19    end;
    1.20