# HG changeset patch
# User blanchet
# Date 1347133937 -7200
# Node ID a9295b1f401b797cc39832b6a7e52c06c40b3bc1
# Parent  60a0394d98f78ecb4f864d0c5b1a74bc0d2b28a0
renamed for consistency

diff -r 60a0394d98f7 -r a9295b1f401b src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- 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"
diff -r 60a0394d98f7 -r a9295b1f401b src/HOL/Codatatype/Tools/bnf_gfp.ML
--- 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 =>