src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58580 8ee2d984caa8
parent 58579 b7bc5ba2f3fb
child 58581 e2e2d775869c
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:40 2014 +0200
     1.3 @@ -477,7 +477,7 @@
     1.4          xtor_co_rec_thms = xtor_co_rec_thms,
     1.5          xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
     1.6          xtor_rel_co_induct = xtor_rel_co_induct,
     1.7 -        dtor_set_induct_thms = [],
     1.8 +        dtor_set_inducts = [],
     1.9          xtor_co_rec_transfer_thms = []}
    1.10         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    1.11    in