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