--- a/src/Pure/General/scan.ML Wed Jun 09 18:55:28 2004 +0200
+++ b/src/Pure/General/scan.ML Wed Jun 09 18:56:09 2004 +0200
@@ -32,6 +32,7 @@
val $$ : ''a -> ''a list -> ''a * ''a list
(*literal list*)
val this: ''a list -> ''a list -> ''a list * ''a list
+ val this_string: string -> string list -> string * string list
end;
signature SCAN =
@@ -159,6 +160,8 @@
if y = x then drop_prefix ys xs else raise FAIL None;
in (ys, drop_prefix ys xs) end;
+fun this_string s = this (explode s) >> (K s);
+
fun any _ [] = raise MORE None
| any pred (lst as x :: xs) =
if pred x then apfst (cons x) (any pred xs)