# 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