# HG changeset patch
# User wenzelm
# Date 1086800169 -7200
# Node ID c77fda9b6cf0599a5b39fb181809d943294c668d
# Parent  2da524f3d785ecabb6eeed019b9678db2829a1c8
added this_string;

diff -r 2da524f3d785 -r c77fda9b6cf0 src/Pure/General/scan.ML
--- 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)