src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML

     Logic.list_implies (assms |> map snd, concl)
       |> subst_free substitutions
       |> thm_of_term ctxt
   end
 
-(* mapping of proof methods to tactics *)
+(* mapping from proof methods to tactics *)
 fun tac_of_method method type_enc lam_trans ctxt facts =
   case method of
     MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
   | _ =>
       Method.insert_tac facts
       THEN' (case method of
               SimpM => Simplifier.asm_full_simp_tac
-            | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt))
+            | AutoM => Clasimp.auto_tac #> K
             | FastforceM => Clasimp.fast_force_tac
             | ForceM => Clasimp.force_tac
             | ArithM => Arith_Data.arith_tac
             | BlastM => blast_tac
             | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt