src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 57700 a2c4adb839a9
parent 57527 1b07ca054327
child 57801 4adfa833072b
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Jul 30 00:50:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Jul 30 10:50:28 2014 +0200
     1.3 @@ -463,7 +463,8 @@
     1.4          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
     1.5          xtor_co_rec_thms = xtor_co_rec_thms,
     1.6          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
     1.7 -        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
     1.8 +        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
     1.9 +        dtor_set_induct_thms = []}
    1.10         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    1.11    in
    1.12      (fp_res, lthy)