src/HOL/Tools/lin_arith.ML
changeset 30240 5b25fee0362c
parent 29850 14d9891c917b
child 30496 7cdcc9dd95cb
--- a/src/HOL/Tools/lin_arith.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Wed Mar 04 10:45:52 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;