--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200
@@ -22,6 +22,7 @@
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_rec: term,
+ co_rec_def: thm,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
@@ -137,6 +138,7 @@
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_rec: term,
+ co_rec_def: thm,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
@@ -161,6 +163,7 @@
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
co_rec = Morphism.term phi co_rec,
+ co_rec_def = Morphism.thm phi co_rec_def,
maps = map (Morphism.thm phi) maps,
common_co_inducts = map (Morphism.thm phi) common_co_inducts,
co_inducts = map (Morphism.thm phi) co_inducts,