--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 08 14:03:01 2014 +0200
@@ -462,7 +462,7 @@
fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, 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 (substAT T) perm_Cs' corec, exhaust_discs = exhaust_discs,
+ {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) 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,
fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,