--- 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;
--- 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