# HG changeset patch
# User blanchet
# Date 1411979979 -7200
# Node ID 4d00caa0e4d742b8c8d05f14c5f184a1e583ff15
# Parent  66ddc5ad4f6335665e9c7f6252f94dd5b358ccd2
tuning

diff -r 66ddc5ad4f63 -r 4d00caa0e4d7 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 29 08:13:23 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 29 10:39:39 2014 +0200
@@ -1124,8 +1124,8 @@
 fun postproc_co_induct lthy nn prop prop_conj =
   Drule.zero_var_indexes
   #> `(conj_dests nn)
-  #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
-  ##> (fn thm => Thm.permute_prems 0 (~nn)
+  #>> map (fn thm => Thm.permute_prems 0 ~1 (thm RS prop))
+  ##> (fn thm => Thm.permute_prems 0 (~ nn)
     (if nn = 1 then thm RS prop
      else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
 
@@ -1524,12 +1524,9 @@
       end
     val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   in
-    map (fn Asets =>
-      let
-        fun massage_thm thm = rotate_prems (~1) (thm RS bspec);
-      in
-        mk_thm lthy fpTs ctrss Asets |> nn = 1 ? map_prod massage_thm (cons consumes_attr)
-      end) (transpose setss)
+    map (mk_thm lthy fpTs ctrss
+        #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr))
+      (transpose setss)
   end;
 
 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))