changeset 30190 | 479806475f3c |
parent 29850 | 14d9891c917b |
child 30496 | 7cdcc9dd95cb |
--- a/src/HOL/Tools/lin_arith.ML Sun Mar 01 16:48:06 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Sun Mar 01 23:36:12 2009 +0100 @@ -672,7 +672,7 @@ let fun filter_prems (t, (left, right)) = if p t then (left, right @ [t]) else (left @ right, []) - val (left, right) = foldl filter_prems ([], []) terms + val (left, right) = List.foldl filter_prems ([], []) terms in right @ left end;