src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49124 968e1b7de057
parent 49123 263b0e330d8b
child 49125 5fc5211cf104
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 13:06:41 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 14:21:11 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 -> Proof.context ->
     1.7 -    term list * Proof.context
     1.8 +    (term list * term list * thm list * thm list) * Proof.context
     1.9  end;
    1.10  
    1.11  structure BNF_GFP : BNF_GFP =
    1.12 @@ -2989,7 +2989,8 @@
    1.13              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.14            bs thmss)
    1.15    in
    1.16 -    (flds, lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.17 +    ((flds, unfs, fld_unf_thms, unf_fld_thms),
    1.18 +      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    1.19    end;
    1.20  
    1.21  val _ =