--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sun Sep 09 12:51:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Sun Sep 09 13:04:57 2012 +0200
@@ -22,7 +22,6 @@
val corecN: string
val exhaustN: string
val fldN: string
- val fld_unf_coitersN: string
val fld_exhaustN: string
val fld_induct2N: string
val fld_inductN: string
@@ -32,6 +31,8 @@
val fld_recN: string
val fld_recsN: string
val fld_unfN: string
+ val fld_unf_coitersN: string
+ val fld_unf_corecsN: string
val hsetN: string
val hset_recN: string
val inductN: string
@@ -166,6 +167,7 @@
val fld_recsN = fld_recN ^ "s"
val unf_corecN = unfN ^ "_" ^ corecN
val unf_corecsN = unf_corecN ^ "s"
+val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s"
val fld_unfN = fldN ^ "_" ^ unfN
val unf_fldN = unfN ^ "_" ^ fldN