src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58448 a1d4e7473c98
parent 58446 e89f57d1e46c
child 58578 9ff8ca957c02
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:54 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:56 2014 +0200
     1.3 @@ -478,7 +478,7 @@
     1.4          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
     1.5          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
     1.6          dtor_set_induct_thms = [],
     1.7 -        ctor_rec_transfer_thms = []}
     1.8 +        xtor_co_rec_transfer_thms = []}
     1.9         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    1.10    in
    1.11      (fp_res, lthy)