src/HOL/Tools/lin_arith.ML
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;