src/HOL/Tools/lin_arith.ML

 (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
 (* terms in the same way as filter_prems_tac does                            *)
 
 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
 let
-  fun filter_prems (t, (left, right)) =
-    if  p t  then  (left, right @ [t])  else  (left @ right, [])
-  val (left, right) = List.foldl filter_prems ([], []) terms
+  fun filter_prems t (left, right) =
+    if p t then (left, right @ [t]) else (left @ right, [])
+  val (left, right) = fold filter_prems terms ([], [])
 in
   right @ left
 end;
 
 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)