src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

   end;
 
 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));
 
 fun mk_induct_attrs ctrss =
   let

       in
         (thm, case_names_attr :: induct_set_attrs)
       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), _))
     dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
     kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)