# HG changeset patch
# User chaieb
# Date 1191867613 -7200
# Node ID eb6fd8f78d56a62b9494a21d61370560cef33fc7
# Parent  52bc004950c4d0f89b47f1f5e799f7ce66b9ffad
fixed bug in grobner_ideal

diff -r 52bc004950c4 -r eb6fd8f78d56 src/HOL/Tools/Groebner_Basis/groebner.ML
--- 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;
 
 (* ------------------------------------------------------------------------- *)