src/HOL/Library/normarith.ML

    val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
            else ()
    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
    fun consider d =
     let