tuned;

--- a/src/Pure/General/ord_list.ML	Sat Jun 18 22:47:44 2005 +0200
+++ b/src/Pure/General/ord_list.ML	Sat Jun 18 22:57:23 2005 +0200
@@ -43,7 +43,7 @@
 fun remove ord x list =
   let
     fun rmove [] = raise SAME
-      | rmove (lst as y :: ys) =
+      | rmove (y :: ys) =
           (case ord (x, y) of
             LESS => raise SAME
           | EQUAL => ys