--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 19 13:27:04 2014 +0200
@@ -21,10 +21,10 @@
fun is_new_datatype ctxt s =
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx,
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx,
co_rec_thms = rec_thms, ...} : fp_sugar) =
- {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms};
+ {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
+ recx = recx, rec_thms = rec_thms};
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let