--- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Apr 29 09:45:14 2013 +0200
@@ -1853,9 +1853,11 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, ctor_induct_thm, dtor_ctor_thms,
- ctor_dtor_thms, ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss',
- ctor_Irel_thms, ctor_fold_thms, ctor_rec_thms),
+ ({bnfs = Ibnfs, dtors = dtors, ctors = ctors, folds = folds, recs = recs,
+ induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+ ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
+ set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,
+ rec_thms = ctor_rec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;