src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58578 9ff8ca957c02
parent 58448 a1d4e7473c98
child 58579 b7bc5ba2f3fb
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:36:48 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:37:38 2014 +0200
     1.3 @@ -388,7 +388,7 @@
     1.4  
     1.5      val co_recs = map (Morphism.term phi) raw_co_recs;
     1.6  
     1.7 -    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
     1.8 +    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
     1.9        |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
    1.10  
    1.11      val xtor_co_rec_thms =
    1.12 @@ -475,7 +475,7 @@
    1.13          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    1.14          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    1.15          xtor_co_rec_thms = xtor_co_rec_thms,
    1.16 -        xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
    1.17 +        xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
    1.18          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
    1.19          dtor_set_induct_thms = [],
    1.20          xtor_co_rec_transfer_thms = []}