renamed for consistency
authorblanchet
Sat Sep 08 21:52:17 2012 +0200 (2012-09-08)
changeset 49225a9295b1f401b
parent 49224 60a0394d98f7
child 49226 510c6d4a73ec
renamed for consistency
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:37:23 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:52:17 2012 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val corecN: string
     1.5    val exhaustN: string
     1.6    val fldN: string
     1.7 -  val fld_unf_coiterN: string
     1.8 +  val fld_unf_coitersN: string
     1.9    val fld_exhaustN: string
    1.10    val fld_induct2N: string
    1.11    val fld_inductN: string
    1.12 @@ -155,7 +155,7 @@
    1.13  val unf_coitersN = unf_coiterN ^ "s"
    1.14  val fld_iter_uniqueN = fld_iterN ^ uniqueN
    1.15  val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
    1.16 -val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN
    1.17 +val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
    1.18  val map_simpsN = mapN ^ "_simps"
    1.19  val map_uniqueN = mapN ^ uniqueN
    1.20  val min_algN = "min_alg"
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:37:23 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:52:17 2012 +0200
     2.3 @@ -2993,7 +2993,7 @@
     2.4          (unf_exhaustN, unf_exhaust_thms),
     2.5          (fld_injectN, fld_inject_thms),
     2.6          (fld_exhaustN, fld_exhaust_thms),
     2.7 -        (fld_unf_coiterN, fld_coiter_thms)]
     2.8 +        (fld_unf_coitersN, fld_coiter_thms)]
     2.9          |> map (apsnd (map single))
    2.10          |> maps (fn (thmN, thmss) =>
    2.11            map2 (fn b => fn thms =>