src/Pure/General/set.ML
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 *)