src/HOL/Tools/lin_arith.ML

 
 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
 (* subgoal that has 'terms' as premises                                      *)
 
 fun negated_term_occurs_positively (terms : term list) : bool =
-  List.exists
+  exists
     (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
       member Envir.aeconv terms (Trueprop $ t)
       | _ => false)
     terms;