--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:15:59 2007 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:16:05 2007 +0100
@@ -316,7 +316,7 @@
let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
val phists = filter (fn (p,_) => not (null p)) npols
val bas = grobner_interreduce [] (map monic phists)
- val prs0 = product bas bas
+ val prs0 = map_product pair bas bas
val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
val prs3 =