diff -r 6793b02a3409 -r ddf1f03a9ad9 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:56 2009 +0200
@@ -620,7 +620,7 @@
   | NONE => (case eqs of 
     [] => 
      let val vars = remove (op aconvc) one_tm 
-           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
+           (fold_rev (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 (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
+      (fold_rev (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)