src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49128 1a86ef0a0210
parent 49126 1bbd7a37fc29
child 49134 846264f80f16
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 16:27:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 17:23:08 2012 +0200
     1.3 @@ -1938,7 +1938,7 @@
     1.4  
     1.5      val timer = time (timer "unf definitions & thms");
     1.6  
     1.7 -    fun coiter_bind i = Binding.suffix_name ("_" ^ coN ^ iterN) (nth bs (i - 1));
     1.8 +    fun coiter_bind i = Binding.suffix_name ("_" ^ unf_coiterN) (nth bs (i - 1));
     1.9      val coiter_name = Binding.name_of o coiter_bind;
    1.10      val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind;
    1.11  
    1.12 @@ -2129,7 +2129,7 @@
    1.13            trans OF [mor RS unique, coiter_unf]) coiter_unique_mor_thms coiter_unf_thms
    1.14        end;
    1.15  
    1.16 -    fun corec_bind i = Binding.suffix_name ("_" ^ coN ^ recN) (nth bs (i - 1));
    1.17 +    fun corec_bind i = Binding.suffix_name ("_" ^ unf_corecN) (nth bs (i - 1));
    1.18      val corec_name = Binding.name_of o corec_bind;
    1.19      val corec_def_bind = rpair [] o Thm.def_binding o corec_bind;
    1.20  
    1.21 @@ -2973,16 +2973,16 @@
    1.22            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    1.23  
    1.24        val notes =
    1.25 -        [(coiterN, coiter_thms),
    1.26 -        (coiter_uniqueN, coiter_unique_thms),
    1.27 -        (corecN, corec_thms),
    1.28 +        [(unf_coiterN, coiter_thms),
    1.29 +        (unf_coiter_uniqueN, coiter_unique_thms),
    1.30 +        (unf_corecN, corec_thms),
    1.31          (unf_fldN, unf_fld_thms),
    1.32          (fld_unfN, fld_unf_thms),
    1.33          (unf_injectN, unf_inject_thms),
    1.34          (unf_exhaustN, unf_exhaust_thms),
    1.35          (fld_injectN, fld_inject_thms),
    1.36          (fld_exhaustN, fld_exhaust_thms),
    1.37 -        (fld_coiterN, fld_coiter_thms)]
    1.38 +        (fld_unf_coiterN, fld_coiter_thms)]
    1.39          |> map (apsnd (map single))
    1.40          |> maps (fn (thmN, thmss) =>
    1.41            map2 (fn b => fn thms =>