src/HOL/Tools/Groebner_Basis/groebner.ML
changeset 24913 eb6fd8f78d56
parent 24630 351a308ab58d
child 25251 759bffe1d416
--- 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;
 
 (* ------------------------------------------------------------------------- *)