src/HOL/Tools/Groebner_Basis/groebner.ML

 (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)
 (* ------------------------------------------------------------------------- *)
 
 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;
 
 (* ------------------------------------------------------------------------- *)
 (* Produce Strong Nullstellensatz certificate for a power of pol.            *)
 (* ------------------------------------------------------------------------- *)