diff -r 6d8d5fe9f3a2 -r cbe8c859817c src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:21:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:30:31 2012 +0200
@@ -28,7 +28,9 @@
   val fld_inductN: string
   val fld_injectN: string
   val fld_iterN: string
+  val fld_itersN: string
   val fld_recN: string
+  val fld_recsN: string
   val fld_unfN: string
   val hsetN: string
   val hset_recN: string
@@ -59,7 +61,9 @@
   val unf_coinductN: string
   val unf_coinduct_uptoN: string
   val unf_coiterN: string
+  val unf_coitersN: string
   val unf_corecN: string
+  val unf_corecsN: string
   val unf_exhaustN: string
   val unf_fldN: string
   val unf_injectN: string
@@ -146,7 +150,9 @@
 val fldN = "fld"
 val unfN = "unf"
 val fld_iterN = fldN ^ "_" ^ iterN
+val fld_itersN = fld_iterN ^ "s"
 val unf_coiterN = unfN ^ "_" ^ coiterN
+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
@@ -172,7 +178,9 @@
 val recN = "rec"
 val corecN = coN ^ recN
 val fld_recN = fldN ^ "_" ^ recN
+val fld_recsN = fld_recN ^ "s"
 val unf_corecN = unfN ^ "_" ^ corecN
+val unf_corecsN = unf_corecN ^ "s"
 
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN