src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 58118 0a58bff4939d
parent 58117 9608028d8f43
child 58131 1abeda3c3bc2
--- 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,