diff -r ec5b4ab52026 -r 2443224cf6d7 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Jun 12 10:15:40 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Jun 12 10:15:45 2007 +0200
@@ -12,6 +12,7 @@
     Conv.conv ->  Conv.conv ->
     Conv.conv * (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list)
     val ring_conv : Proof.context -> cterm -> thm
+    val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
 end
 
 structure Groebner: GROEBNER =
@@ -275,8 +276,8 @@
 
 
 fun grobner_basis basis pairs =
-  (writeln (Int.toString(length basis)^" basis elements and "^
-               Int.toString(length pairs)^" critical pairs");
+  ((* writeln (Int.toString(length basis)^" basis elements and "^
+               Int.toString(length pairs)^" critical pairs"); *)
   case pairs of
     [] => basis
   | (l,(p1,p2))::opairs =>
@@ -652,7 +653,7 @@
        val th2 = funpow (Integer.machine_int deg) (idom_rule o conji th1) neq_01
       in (vars,l,cert,th2)
       end)
-    val _ = writeln ("Translating certificate to HOL inferences")
+(*    val _ = writeln ("Translating certificate to HOL inferences") *)
     val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
     val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
                                             (filter (fn (c,m) => c </ rat_0) p))) cert
@@ -742,4 +743,16 @@
           dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt)
           (semiring_normalize_wrapper ctxt res)) form));
 
+fun algebra_tac add_ths del_ths ctxt i = ObjectLogic.full_atomize_tac i 
+  THEN (simp_tac (fst (NormalizerData.get ctxt) delsimps del_ths addsimps add_ths) i)
+  THEN (fn st =>
+   case try (nth (cprems_of st)) (i - 1) of
+    NONE => no_tac st
+  | SOME p => let val th = ring_conv ctxt (Thm.dest_arg p)
+              in rtac th i st end
+              handle TERM _ => no_tac st
+                   | THM _ => no_tac st
+                   | ERROR _ => no_tac st
+                   | CTERM _ => no_tac st);
+
 end;