diff -r c7225307acf2 -r 383a5b9efbd0 src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Fri Aug 26 21:18:42 2011 +0200
+++ b/src/Pure/General/linear_set.ML	Fri Aug 26 21:27:58 2011 +0200
@@ -16,10 +16,8 @@
   val defined: 'a T -> key -> bool
   val lookup: 'a T -> key -> ('a * key option) option
   val update: key * 'a -> 'a T -> 'a T
-  val fold: key option ->
+  val iterate: key option ->
     ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
-  val get_first: key option ->
-    ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
   val get_after: 'a T -> key option -> key option
   val insert_after: key option -> key * 'a -> 'a T -> 'a T
   val delete_after: key option -> 'a T -> 'a T
@@ -81,7 +79,7 @@
 fun optional_start set NONE = start_of set
   | optional_start _ some = some;
 
-fun fold opt_start f set =
+fun iterate opt_start f set =
   let
     val entries = entries_of set;
     fun apply _ NONE y = y
@@ -96,17 +94,6 @@
           end;
   in apply NONE (optional_start set opt_start) end;
 
-fun get_first opt_start P set =
-  let
-    val entries = entries_of set;
-    fun first _ NONE = NONE
-      | first prev (SOME key) =
-          let
-            val (x, next) = the_entry entries key;
-            val item = ((prev, key), x);
-          in if P item then SOME item else first (SOME key) next end;
-  in first NONE (optional_start set opt_start) end;
-
 
 (* relative addressing *)