--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Apr 29 09:45:14 2013 +0200
@@ -3029,9 +3029,12 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((Jbnfs, dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_strong_coinduct_thm,
- dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms, folded_dtor_map_thms,
- folded_dtor_set_thmss', dtor_Jrel_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
+ ({bnfs = Jbnfs, dtors = dtors, ctors = ctors, folds = unfolds, recs = corecs,
+ induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm,
+ dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
+ map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',
+ rel_thms = dtor_Jrel_thms, fold_thms = ctor_dtor_unfold_thms,
+ rec_thms = ctor_dtor_corec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;