# HG changeset patch
# User wenzelm
# Date 1085835964 -7200
# Node ID 30556b84af7c03c5bf660fa511fe3212ee626b26
# Parent  6589a58f57cb0064ee0292ed751b45842d53151b
Output.error;

diff -r 6589a58f57cb -r 30556b84af7c src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat May 29 15:05:51 2004 +0200
+++ b/src/Pure/General/scan.ML	Sat May 29 15:06:04 2004 +0200
@@ -31,7 +31,7 @@
   (*one element literal*)
   val $$ : ''a -> ''a list -> ''a * ''a list
   (*literal list*)
-  val list: ''a list -> ''a list -> ''a list * ''a list
+  val this: ''a list -> ''a list -> ''a list * ''a list
 end;
 
 signature SCAN =
@@ -151,7 +151,7 @@
   | $$ a (x :: xs) =
       if a = x then (x, xs) else raise FAIL None;
 
-fun list ys xs =
+fun this ys xs =
   let
     fun drop_prefix [] xs = xs
       | drop_prefix (_ :: _) [] = raise MORE None
@@ -225,7 +225,7 @@
 fun force scan xs = scan xs handle MORE _ => raise FAIL None;
 fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
 fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
-fun error scan xs = scan xs handle ABORT msg => Library.error msg;
+fun error scan xs = scan xs handle ABORT msg => Output.error msg;
 
 
 (* finite scans *)