diff -r ed495a5088c6 -r 6fe9fd75f9d7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
@@ -15,7 +15,7 @@
 
   datatype proof_method =
     Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
-    Arith_Method | Blast_Method | Meson_Method
+    Arith_Method | Blast_Method | Meson_Method | Algebra_Method
 
   datatype isar_proof =
     Proof of (string * typ) list * (label * term) list * isar_step list
@@ -66,7 +66,7 @@
 
 datatype proof_method =
   Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
-  Arith_Method | Blast_Method | Meson_Method
+  Arith_Method | Blast_Method | Meson_Method | Algebra_Method
 
 datatype isar_proof =
   Proof of (string * typ) list * (label * term) list * isar_step list
@@ -92,7 +92,8 @@
   | Force_Method => "force"
   | Arith_Method => "arith"
   | Blast_Method => "blast"
-  | Meson_Method => "meson")
+  | Meson_Method => "meson"
+  | Algebra_Method => "algebra")
 
 fun steps_of_proof (Proof (_, _, steps)) = steps