src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49222 cbe8c859817c
parent 49213 975ccb0130cb
child 49225 a9295b1f401b
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:21:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:30:31 2012 +0200
     1.3 @@ -2984,9 +2984,9 @@
     1.4            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
     1.5  
     1.6        val notes =
     1.7 -        [(unf_coiterN, coiter_thms),
     1.8 +        [(unf_coitersN, coiter_thms),
     1.9          (unf_coiter_uniqueN, coiter_unique_thms),
    1.10 -        (unf_corecN, corec_thms),
    1.11 +        (unf_corecsN, corec_thms),
    1.12          (unf_fldN, unf_fld_thms),
    1.13          (fld_unfN, fld_unf_thms),
    1.14          (unf_injectN, unf_inject_thms),