changeset 77910 | 10c09fb5a874 |
parent 77851 | ec50b9213969 |
child 77912 | 430e6c477ba4 |
--- a/src/Pure/library.ML Sun Apr 23 19:51:46 2023 +0200 +++ b/src/Pure/library.ML Sun Apr 23 19:57:40 2023 +0200 @@ -820,9 +820,9 @@ fun member eq list x = let - fun memb [] = false - | memb (y :: ys) = eq (x, y) orelse memb ys; - in memb list end; + fun mem [] = false + | mem (y :: ys) = eq (x, y) orelse mem ys; + in mem list end; fun insert eq x xs = if member eq xs x then xs else x :: xs; fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;