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