src/HOL/Library/positivstellensatz.ML
changeset 33063 4d462963a7db
parent 33042 ddf1f03a9ad9
child 33443 b9bbd0f3dcdb
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -643,9 +643,9 @@
     1.4  
     1.5    fun linear_prover (eq,le,lt) = 
     1.6     let 
     1.7 -    val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq - 1))
     1.8 -    val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le - 1))
     1.9 -    val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt - 1))
    1.10 +    val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
    1.11 +    val les = map_index (fn (n, p) => (p,Axiom_le n)) le
    1.12 +    val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
    1.13     in linear_eqs(eqs,les,lts)
    1.14     end 
    1.15