# HG changeset patch
# User wenzelm
# Date 1248540912 -7200
# Node ID d77476e4040cadeb10a6368eee10307bad6c70fe
# Parent  966e166d039d97bb80dd3ee5c3bbe7db45ce97f6
eliminated obsolete/obscure Seq.wrap, Position.setmp_thread_data_seq;

diff -r 966e166d039d -r d77476e4040c src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Jul 25 18:04:15 2009 +0200
+++ b/src/Pure/General/position.ML	Sat Jul 25 18:55:12 2009 +0200
@@ -36,7 +36,6 @@
   val range: T -> T -> range
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
-  val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
 end;
 
 structure Position: POSITION =
@@ -176,9 +175,6 @@
   if ! Output.debugging then f x
   else Library.setmp_thread_data tag (thread_data ()) pos f x;
 
-fun setmp_thread_data_seq pos f x =
-  setmp_thread_data pos f x |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
-
 end;
 
 end;
diff -r 966e166d039d -r d77476e4040c src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Sat Jul 25 18:04:15 2009 +0200
+++ b/src/Pure/General/seq.ML	Sat Jul 25 18:55:12 2009 +0200
@@ -33,7 +33,6 @@
   val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
   val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
   val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq
-  val wrap: ((unit -> ('a * 'a seq) option) -> ('a * 'a seq) option) -> 'a seq -> 'a seq
   val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
   val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
   val succeed: 'a -> 'a seq
@@ -170,13 +169,6 @@
 
 fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
 
-(*wrapped lazy evaluation*)
-fun wrap f xq =
-  make (fn () =>
-    (case f (fn () => pull xq) of
-      NONE => NONE
-    | SOME (x, xq') => SOME (x, wrap f xq')));
-
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =
   let