src/HOL/Codatatype/Tools/bnf_fp.ML

   val caseN: string
   val coN: string
   val coinductN: string
   val coiterN: string
   val coitersN: string
-  val coiter_iffN: string
   val corecN: string
   val corecsN: string
-  val corec_iffN: string
+  val disc_coiter_iffN: string
   val disc_coitersN: string
+  val disc_corec_iffN: string
   val disc_corecsN: string
   val exhaustN: string
   val fldN: string
   val fld_exhaustN: string
   val fld_induct2N: string

 val caseN = "case"
 val discN = "disc"
 val disc_coitersN = discN ^ "_" ^ coitersN
 val disc_corecsN = discN ^ "_" ^ corecsN
 val iffN = "_iff"
-val coiter_iffN = coiterN ^ iffN
-val corec_iffN = corecN ^ iffN
+val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN
+val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
 val selN = "sel"
 val sel_coitersN = selN ^ "_" ^ coitersN
 val sel_corecsN = selN ^ "_" ^ corecsN
 
 val mk_common_name = space_implode "_" o map Binding.name_of;