src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
changeset 58584 b6492a7abb59
parent 58583 1dd83cbba636
child 58585 efc8b2c54a38
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:40:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:40:56 2014 +0200
@@ -42,7 +42,7 @@
    ctor_injects = @{thms xtor_inject},
    dtor_injects = @{thms xtor_inject},
    xtor_maps = [xtor_map],
-   xtor_set_thmss = [xtor_sets],
+   xtor_setss = [xtor_sets],
    xtor_rel_thms = [xtor_rel],
    xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
    xtor_co_rec_o_maps = [ctor_rec_o_map],