src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58585 efc8b2c54a38
parent 58584 b6492a7abb59
child 58634 9f10d82e8188
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:41:37 2014 +0200
@@ -473,7 +473,7 @@
         dtor_injects = of_fp_res #dtor_injects (*too general types*),
         xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
         xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
-        xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
+        xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
         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,