# HG changeset patch # User wenzelm # Date 1119127664 -7200 # Node ID 287514d817631407fe3f8b75d5e0ca153479a977 # Parent 82e2fc13ce5461dbea704f003951b6f7964ad5a1 tuned remove; diff -r 82e2fc13ce54 -r 287514d81763 src/Pure/General/ord_list.ML --- a/src/Pure/General/ord_list.ML Sat Jun 18 22:42:01 2005 +0200 +++ b/src/Pure/General/ord_list.ML Sat Jun 18 22:47:44 2005 +0200 @@ -42,7 +42,7 @@ fun remove ord x list = let - fun rmove [] = [] + fun rmove [] = raise SAME | rmove (lst as y :: ys) = (case ord (x, y) of LESS => raise SAME