changeset 53808 | b3e2022530e3 |
parent 53747 | a8253329ebe9 |
child 53901 | 3d93e8b4ae02 |
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Sep 24 00:01:10 2013 +0200 @@ -131,7 +131,7 @@ val all_notes = (case lfp_sugar_thms of NONE => [] - | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) => + | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) => let val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])