src/HOL/Library/positivstellensatz.ML
changeset 33038 8f9594c31de4
parent 33002 f3f02f36a3e2
child 33039 5018f6a76b3f
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -568,7 +568,7 @@
     1.4    fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
     1.5    val one_tm = @{cterm "1::real"}
     1.6    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
     1.7 -     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
     1.8 +     ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
     1.9         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    1.10  
    1.11    fun linear_ineqs vars (les,lts) = 
    1.12 @@ -620,7 +620,7 @@
    1.13    | NONE => (case eqs of 
    1.14      [] => 
    1.15       let val vars = remove (op aconvc) one_tm 
    1.16 -           (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
    1.17 +           (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
    1.18       in linear_ineqs vars (les,lts) end
    1.19     | (e,p)::es => 
    1.20       if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
    1.21 @@ -679,7 +679,7 @@
    1.22    val le_pols = map rhs le
    1.23    val lt_pols = map rhs lt 
    1.24    val aliens =  filter is_alien
    1.25 -      (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    1.26 +      (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
    1.27            (eq_pols @ le_pols @ lt_pols) [])
    1.28    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    1.29    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)