diff -r d406979024d1 -r 8ea4bad49ed5 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 23:06:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 23:06:39 2012 +0200
@@ -18,7 +18,6 @@
   val caseN: string
   val coN: string
   val coinductN: string
-  val coinductsN: string
   val coiterN: string
   val coitersN: string
   val corecN: string
@@ -42,7 +41,6 @@
   val hsetN: string
   val hset_recN: string
   val inductN: string
-  val inductsN: string
   val injectN: string
   val isNodeN: string
   val iterN: string
@@ -159,7 +157,9 @@
 val algN = "alg"
 val IITN = "IITN"
 val iterN = "iter"
+val itersN = iterN ^ "s"
 val coiterN = coN ^ iterN
+val coitersN = coiterN ^ "s"
 val uniqueN = "_unique"
 val fldN = "fld"
 val unfN = "unf"
@@ -190,7 +190,9 @@
 
 val str_initN = "str_init"
 val recN = "rec"
+val recsN = recN ^ "s"
 val corecN = coN ^ recN
+val corecsN = corecN ^ "s"
 val fld_recN = fldN ^ "_" ^ recN
 val fld_recsN = fld_recN ^ "s"
 val unf_corecN = unfN ^ "_" ^ corecN
@@ -226,16 +228,12 @@
 val set_set_inclN = "set_set_incl"
 
 val caseN = "case"
-val coinductsN = "coinducts"
-val coitersN = "coiters"
-val corecsN = "corecs"
-val disc_coitersN = "disc_coiters"
-val disc_corecsN = "disc_corecs"
-val inductsN = "inducts"
-val itersN = "iters"
-val recsN = "recs"
-val sel_coitersN = "sel_coiters"
-val sel_corecsN = "sel_corecs"
+val discN = "disc"
+val disc_coitersN = discN ^ "_" ^ coitersN
+val disc_corecsN = discN ^ "_" ^ corecsN
+val selN = "sel"
+val sel_coitersN = selN ^ "_" ^ coitersN
+val sel_corecsN = selN ^ "_" ^ corecsN
 
 val mk_common_name = space_implode "_" o map Binding.name_of;