--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100
@@ -163,7 +163,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), (rec_thmss, _)) =>
let
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -172,8 +172,7 @@
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
val notes =
- [(foldN, fold_thmss, []),
- (inductN, map single induct_thms, induct_attrs),
+ [(inductN, map single induct_thms, induct_attrs),
(recN, rec_thmss, code_nitpicksimp_simp_attrs)]
|> filter_out (null o #2)
|> maps (fn (thmN, thmss, attrs) =>