src/HOL/Import/lazy_seq.ML

 	       | SOME (x', _) => SOME(x',Seq (value NONE)))
 
 (*partial function as procedure*)
 fun try f x =
     make (fn () =>
-	     case Library.try f x of
+	     case Basics.try f x of
 		 SOME y => SOME(y,Seq (value NONE))
 	       | NONE => NONE)
 
 (*functional to print a sequence, up to "count" elements;
   the function prelem should print the element number and also the element*)

     if n <= 0
     then ([], xq)
     else
 	case getItem xq of
 	    NONE => ([], xq)
-	  | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
+	  | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
 
 fun foldl f e s =
     let
 	fun F k NONE = k e
 	  | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)