--- 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