--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 22:01:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 08:48:59 2013 +0200
@@ -1856,13 +1856,13 @@
bs thmss)
in
timer;
- ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
- xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm,
+ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
+ xtor_co_induct = ctor_induct_thm,
xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss',
- xtor_rel_thms = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
- xtor_co_rec_thms = ctor_rec_thms},
+ xtor_rel_thms = ctor_Irel_thms,
+ xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;