src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

     | Auto_Method => K (Clasimp.auto_tac ctxt)
     | Fastforce_Method => Clasimp.fast_force_tac ctxt
     | Force_Method => Clasimp.force_tac ctxt
     | Arith_Method => Arith_Data.arith_tac ctxt
     | Blast_Method => blast_tac ctxt
+    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
 fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
   | preplay_raw debug type_enc lam_trans ctxt timeout