--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 11:58:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 12:35:02 2013 +0200
@@ -3029,7 +3029,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ({bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs,
+ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, 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',