tuned;
authorwenzelm
Sat Jun 18 22:57:23 2005 +0200 (2005-06-18)
changeset 16468452cd9ad3eda
parent 16467 287514d81763
child 16469 7e27422c603e
tuned;
src/Pure/General/ord_list.ML
     1.1 --- a/src/Pure/General/ord_list.ML	Sat Jun 18 22:47:44 2005 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Sat Jun 18 22:57:23 2005 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  fun remove ord x list =
     1.5    let
     1.6      fun rmove [] = raise SAME
     1.7 -      | rmove (lst as y :: ys) =
     1.8 +      | rmove (y :: ys) =
     1.9            (case ord (x, y) of
    1.10              LESS => raise SAME
    1.11            | EQUAL => ys