src/HOL/Library/normarith.ML
changeset 33042 ddf1f03a9ad9
parent 33039 5018f6a76b3f
child 33043 ff71cadefb14
     1.1 --- a/src/HOL/Library/normarith.ML	Wed Oct 21 12:02:19 2009 +0200
     1.2 +++ b/src/HOL/Library/normarith.ML	Wed Oct 21 12:02:56 2009 +0200
     1.3 @@ -286,7 +286,7 @@
     1.4     val dests = distinct (op aconvc) (map snd rawdests)
     1.5     val srcfuns = map vector_lincomb sources
     1.6     val destfuns = map vector_lincomb dests 
     1.7 -   val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     1.8 +   val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
     1.9     val n = length srcfuns
    1.10     val nvs = 1 upto n
    1.11     val srccombs = srcfuns ~~ nvs