Output.error;
authorwenzelm
Sat, 29 May 2004 15:06:04 +0200
changeset 14833 30556b84af7c
parent 14832 6589a58f57cb
child 14834 e47744683560
Output.error;
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 *)