--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 13 22:29:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Aug 14 13:20:54 2014 +0200
@@ -471,7 +471,7 @@
#>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
##> (fn thm => Thm.permute_prems 0 (~nn)
(if nn = 1 then thm RS prop
- else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
+ else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
fun mk_induct_attrs ctrss =
let