src/Pure/General/scan.ML

   val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
   (*concatenation*)
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
   (*one element literal*)
   val $$ : ''a -> ''a list -> ''a * ''a list
+  (*literal list*)
+  val list: ''a list -> ''a list -> ''a list * ''a list
 end;
 
 signature SCAN =
 sig
   include BASIC_SCAN

 
 fun $$ _ [] = raise MORE None
   | $$ a (x :: xs) =
       if a = x then (x, xs) else raise FAIL None;
 
+fun list ys xs =
+  let
+    fun drop_prefix [] xs = xs
+      | drop_prefix (_ :: _) [] = raise MORE None
+      | drop_prefix (y :: ys) (x :: xs) =
+          if y = x then drop_prefix ys xs else raise FAIL None;
+  in (ys, drop_prefix ys xs) end;
+
 fun any _ [] = raise MORE None
   | any pred (lst as x :: xs) =
       if pred x then apfst (cons x) (any pred xs)
       else ([], lst);