# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID 4d408eb71301608e299191ebb6f17d8608fe533c
# Parent  bc35a30cf0f28f153a9a25fd6f246d487d3208f6
tuning

diff -r bc35a30cf0f2 -r 4d408eb71301 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 19 13:27:04 2014 +0200
@@ -32,7 +32,6 @@
      fp_res_index: int,
      C: typ,
      fun_arg_Tsss : typ list list list,
-     ctr_defs: thm list,
      ctr_sugar: Ctr_Sugar.ctr_sugar,
      recx: term,
      rec_thms: thm list};
@@ -109,7 +108,6 @@
    fp_res_index: int,
    C: typ,
    fun_arg_Tsss : typ list list list,
-   ctr_defs: thm list,
    ctr_sugar: ctr_sugar,
    recx: term,
    rec_thms: thm list};
diff -r bc35a30cf0f2 -r 4d408eb71301 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- 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