changeset 77741 | 1951f6470792 |
parent 77740 | 19c539f5d4d3 |
child 77742 | 676713cba24d |
--- a/src/Pure/General/set.ML Wed Mar 29 12:02:34 2023 +0200 +++ b/src/Pure/General/set.ML Wed Mar 29 12:05:56 2023 +0200 @@ -13,7 +13,6 @@ val empty: T val build: (T -> T) -> T val is_empty: T -> bool - val is_single: T -> bool val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a val dest: T -> elem list @@ -107,9 +106,6 @@ fun is_empty Empty = true | is_empty _ = false; -fun is_single (Leaf1 _) = true - | is_single _ = false; - (* fold combinators *)