--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Mon Oct 08 19:53:09 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Mon Oct 08 20:20:13 2007 +0200
@@ -357,7 +357,7 @@
fun grobner_ideal vars pols pol =
let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in
- if not (null pol) then error "grobner_ideal: not in the ideal" else
+ if not (null pol') then error "grobner_ideal: not in the ideal" else
resolve_proof vars h end;
(* ------------------------------------------------------------------------- *)