# HG changeset patch
# User blanchet
# Date 1409581067 -7200
# Node ID 0a58bff4939d5c95720dbede77d0dc616be3f530
# Parent  9608028d8f43e2dd3b64083d3aa872e79cba9242
compile

diff -r 9608028d8f43 -r 0a58bff4939d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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,