# HG changeset patch
# User wenzelm
# Date 1119128243 -7200
# Node ID 452cd9ad3eda6bbf91f36e45a66bafc2edae0de6
# Parent  287514d817631407fe3f8b75d5e0ca153479a977
tuned;

diff -r 287514d81763 -r 452cd9ad3eda src/Pure/General/ord_list.ML
--- 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