src/HOL/BNF/Tools/bnf_gfp_tactics.ML

           rtac trans_fun_cong_image_id_id_apply, atac])
       (drop m set_naturals)])
   (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
 
 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
-  {context = ctxt, prems = _} =
+  {context = ctxt, prems = _: thm list} =
   let
     val n = length map_comps;
   in
     unfold_thms_tac ctxt [mor_def] THEN
     EVERY' [rtac conjI,