# 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