--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
@@ -101,6 +101,7 @@
| 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 *)