src/HOL/Library/positivstellensatz.ML
changeset 33042 ddf1f03a9ad9
parent 33039 5018f6a76b3f
child 33063 4d462963a7db
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:19 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 12:02:56 2009 +0200
     1.3 @@ -620,7 +620,7 @@
     1.4    | NONE => (case eqs of 
     1.5      [] => 
     1.6       let val vars = remove (op aconvc) one_tm 
     1.7 -           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
     1.8 +           (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
     1.9       in linear_ineqs vars (les,lts) end
    1.10     | (e,p)::es => 
    1.11       if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
    1.12 @@ -679,7 +679,7 @@
    1.13    val le_pols = map rhs le
    1.14    val lt_pols = map rhs lt 
    1.15    val aliens =  filter is_alien
    1.16 -      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    1.17 +      (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) 
    1.18            (eq_pols @ le_pols @ lt_pols) [])
    1.19    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    1.20    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)