Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/normarith.ML
changeset 33039 5018f6a76b3f
parent 33035 15eab423e573
parent 33038 8f9594c31de4
child 33040 cffdb7b28498
child 33042 ddf1f03a9ad9 
--- a/src/HOL/Library/normarith.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Library/normarith.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -286,7 +286,7 @@
    val dests = distinct (op aconvc) (map snd rawdests)
    val srcfuns = map vector_lincomb sources
    val destfuns = map vector_lincomb dests 
-   val vvs = fold_rev (curry (gen_union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
+   val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
    val n = length srcfuns
    val nvs = 1 upto n
    val srccombs = srcfuns ~~ nvs
isabelle