diff -r 0baf1d9c6780 -r d746a8c12c43 src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Thu Oct 23 13:52:28 2008 +0200
+++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 23 14:22:16 2008 +0200
@@ -80,13 +80,13 @@
 structure LazySeq :> LAZY_SEQ =
 struct
 
-datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
+datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
 
 exception Empty
 
-fun getItem (Seq s) = Susp.force s
+fun getItem (Seq s) = Lazy.force s
 val pull = getItem
-fun make f = Seq (Susp.delay f)
+fun make f = Seq (Lazy.lazy f)
 
 fun null s = is_none (getItem s)
 
@@ -137,7 +137,7 @@
 local
     fun F NONE _ = raise Subscript
       | F (SOME(x,s)) n = SOME(x,F' s (n-1))
-    and F' s 0 = Seq (Susp.value NONE)
+    and F' s 0 = Seq (Lazy.value NONE)
       | F' s n = make (fn () => F (getItem s) n)
 in
 fun take (s,n) =
@@ -166,14 +166,14 @@
 
 local
     fun F s NONE = s
-      | F s (SOME(x,s')) = F (SOME(x, Seq (Susp.value s))) (getItem s')
+      | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
 in
 fun rev s = make (fn () => F NONE (getItem s))
 end
 
 local
     fun F s NONE = getItem s
-      | F s (SOME(x,s')) = F (Seq (Susp.value (SOME(x,s)))) (getItem s')
+      | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
 in
 fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
 end
@@ -294,13 +294,13 @@
 	F' s1 s2
     end
 
-fun empty  _ = Seq (Susp.value NONE)
-fun single x = Seq(Susp.value (SOME(x,Seq (Susp.value NONE))))
-fun cons a = Seq(Susp.value (SOME a))
+fun empty  _ = Seq (Lazy.value NONE)
+fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
+fun cons a = Seq(Lazy.value (SOME a))
 
 fun cycle seqfn =
     let
-	val knot = ref (Seq (Susp.value NONE))
+	val knot = ref (Seq (Lazy.value NONE))
     in
 	knot := seqfn (fn () => !knot);
 	!knot
@@ -374,7 +374,7 @@
 (* Adapted from seq.ML *)
 
 val succeed = single
-fun fail _ = Seq (Susp.value NONE)
+fun fail _ = Seq (Lazy.value NONE)
 
 (* fun op THEN (f, g) x = flat (map g (f x)) *)
 
@@ -414,7 +414,7 @@
 fun TRY f x =
     make (fn () =>
 	     case getItem (f x) of
-		 NONE => SOME(x,Seq (Susp.value NONE))
+		 NONE => SOME(x,Seq (Lazy.value NONE))
 	       | some => some)
 
 fun REPEAT f =
@@ -446,13 +446,13 @@
     make (fn () =>
 	     case getItem (f x) of
 		 NONE => NONE
-	       | SOME (x', _) => SOME(x',Seq (Susp.value NONE)))
+	       | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
 
 (*partial function as procedure*)
 fun try f x =
     make (fn () =>
 	     case Basics.try f x of
-		 SOME y => SOME(y,Seq (Susp.value NONE))
+		 SOME y => SOME(y,Seq (Lazy.value NONE))
 	       | NONE => NONE)
 
 (*functional to print a sequence, up to "count" elements;
@@ -497,7 +497,7 @@
 
 (*turn a list of sequences into a sequence of lists*)
 local
-    fun F [] = SOME([],Seq (Susp.value NONE))
+    fun F [] = SOME([],Seq (Lazy.value NONE))
       | F (xq :: xqs) =
         case getItem xq of
             NONE => NONE