diff -r b458558cbcc2 -r fa3a1ec69a1b src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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
@@ -146,8 +146,8 @@
       (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
 
     val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
-    val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
-    val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
+    val recs = map (fst o dest_Const o #co_rec) fp_sugars;
+    val rec_thms = maps #co_rec_thms fp_sugars;
 
     fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
         distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =