--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:37:23 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sat Sep 08 21:52:17 2012 +0200
@@ -22,7 +22,7 @@
val corecN: string
val exhaustN: string
val fldN: string
- val fld_unf_coiterN: string
+ val fld_unf_coitersN: string
val fld_exhaustN: string
val fld_induct2N: string
val fld_inductN: string
@@ -155,7 +155,7 @@
val unf_coitersN = unf_coiterN ^ "s"
val fld_iter_uniqueN = fld_iterN ^ uniqueN
val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
-val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN
+val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
val map_simpsN = mapN ^ "_simps"
val map_uniqueN = mapN ^ uniqueN
val min_algN = "min_alg"
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Sat Sep 08 21:37:23 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Sat Sep 08 21:52:17 2012 +0200
@@ -2993,7 +2993,7 @@
(unf_exhaustN, unf_exhaust_thms),
(fld_injectN, fld_inject_thms),
(fld_exhaustN, fld_exhaust_thms),
- (fld_unf_coiterN, fld_coiter_thms)]
+ (fld_unf_coitersN, fld_coiter_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>