--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 01 16:17:47 2014 +0200
@@ -461,8 +461,8 @@
end;
fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
- co_rec_thms = corec_thms, disc_co_recs = corec_discs,
- sel_co_recss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ co_rec_thms = corec_thms, co_rec_discs = corec_discs,
+ co_rec_selss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
{corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
sel_defs = sel_defs,
fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,