diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -568,7 +568,7 @@
   fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
   val one_tm = @{cterm "1::real"}
   fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
-     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
+     ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
        not(p(FuncUtil.Ctermfunc.apply e one_tm)))
 
   fun linear_ineqs vars (les,lts) = 
@@ -620,7 +620,7 @@
   | NONE => (case eqs of 
     [] => 
      let val vars = remove (op aconvc) one_tm 
-           (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
+           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
      in linear_ineqs vars (les,lts) end
    | (e,p)::es => 
      if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
@@ -679,7 +679,7 @@
   val le_pols = map rhs le
   val lt_pols = map rhs lt 
   val aliens =  filter is_alien
-      (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
+      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
           (eq_pols @ le_pols @ lt_pols) [])
   val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)