diff -r 709e1d671483 -r e8a87398f35d src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/General/linear_set.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -14,7 +14,7 @@
   val empty: 'a T
   val is_empty: 'a T -> bool
   val defined: 'a T -> key -> bool
-  val lookup: 'a T -> key -> 'a option
+  val lookup: 'a T -> key -> ('a * key option) option
   val update: key * 'a -> 'a T -> 'a T
   val fold: key option ->
     ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
@@ -70,7 +70,7 @@
 
 fun defined set key = Table.defined (entries_of set) key;
 
-fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+fun lookup set key = Table.lookup (entries_of set) key;
 
 fun update (key, x) = map_set (fn (start, entries) =>
   (start, put_entry (key, (x, next_entry entries key)) entries));