--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 01 23:25:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Aug 02 12:08:55 2013 +0200
@@ -2920,7 +2920,8 @@
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
xtor_rel_thms = dtor_Jrel_thms,
- xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms]},
+ xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms],
+ rel_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;