src/HOL/Tools/lin_arith.ML
changeset 33339 d41f77196338
parent 33317 b4534348b8fd
child 33519 e31a85f92ce9
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -645,9 +645,9 @@
     1.4  
     1.5  fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
     1.6  let
     1.7 -  fun filter_prems (t, (left, right)) =
     1.8 -    if  p t  then  (left, right @ [t])  else  (left @ right, [])
     1.9 -  val (left, right) = List.foldl filter_prems ([], []) terms
    1.10 +  fun filter_prems t (left, right) =
    1.11 +    if p t then (left, right @ [t]) else (left @ right, [])
    1.12 +  val (left, right) = fold filter_prems terms ([], [])
    1.13  in
    1.14    right @ left
    1.15  end;