src/Provers/Arith/abel_cancel.ML

        val common = (*inter_term miscounts repetitions, so squash them*)
                     gen_distinct (op aconv) (inter_term (ltms, rtms))
        val _ = if null common then raise Cancel  (*nothing to do*)
                                    else ()
 
-       fun cancelled tms = mk_sum ty (foldl cancel1 (tms, common))
+       fun cancelled tms = mk_sum ty (Library.foldl cancel1 (tms, common))
 
        val lt' = cancelled ltms
        and rt' = cancelled rtms
 
        val rhs = rel$lt'$rt'