# HG changeset patch
# User blanchet
# Date 1456242610 -3600
# Node ID f60085077ab0fcf5b851ef4e9db8375ebba1f001
# Parent  ff5d7a9831ef826f506076b3f34f66454e8dabc5
tuning

diff -r ff5d7a9831ef -r f60085077ab0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Feb 23 16:50:10 2016 +0100
@@ -448,7 +448,7 @@
       | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys;
   in zed [] end;
 
-fun unfla xss = fold_map (fn _ => fn (c :: cs) => (c,cs)) xss;
+fun unfla xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs;
 fun unflat xss = fold_map unfla xss;
 fun unflatt xsss = fold_map unflat xsss;
 fun unflattt xssss = fold_map unflatt xssss;
@@ -2724,7 +2724,7 @@
         ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
       |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types
       |> case_fp fp derive_note_induct_recs_thms_for_types
-           derive_note_coinduct_corecs_thms_for_types;
+        derive_note_coinduct_corecs_thms_for_types;
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       co_prefix fp ^ "datatype"));