--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:43:26 2014 +0200
@@ -408,7 +408,8 @@
val thy = Proof_Context.theory_of lthy0;
val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
- common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+ fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
+ (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
val coinduct_attrs_pair =
@@ -430,7 +431,8 @@
val perm_Ts = map #T perm_fp_sugars;
val perm_Xs = map #X perm_fp_sugars;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
+ val perm_Cs =
+ map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -496,8 +498,8 @@
distinct_discsss collapses corec_thms corec_discs corec_selss
end;
- fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, co_rec = corec,
- fp_co_induct_sugar = {co_rec_thms = corec_thms, co_rec_discs = corec_discs,
+ fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
+ fp_co_induct_sugar = {co_rec = corec, 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 perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
sel_defs = sel_defs,