Output.error;
authorwenzelm
Sat, 29 May 2004 15:06:04 +0200
changeset 1483330556b84af7c
parent 14832 6589a58f57cb
child 14834 e47744683560
Output.error;
src/Pure/General/scan.ML
     1.1 --- a/src/Pure/General/scan.ML	Sat May 29 15:05:51 2004 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Sat May 29 15:06:04 2004 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    (*one element literal*)
     1.5    val $$ : ''a -> ''a list -> ''a * ''a list
     1.6    (*literal list*)
     1.7 -  val list: ''a list -> ''a list -> ''a list * ''a list
     1.8 +  val this: ''a list -> ''a list -> ''a list * ''a list
     1.9  end;
    1.10  
    1.11  signature SCAN =
    1.12 @@ -151,7 +151,7 @@
    1.13    | $$ a (x :: xs) =
    1.14        if a = x then (x, xs) else raise FAIL None;
    1.15  
    1.16 -fun list ys xs =
    1.17 +fun this ys xs =
    1.18    let
    1.19      fun drop_prefix [] xs = xs
    1.20        | drop_prefix (_ :: _) [] = raise MORE None
    1.21 @@ -225,7 +225,7 @@
    1.22  fun force scan xs = scan xs handle MORE _ => raise FAIL None;
    1.23  fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
    1.24  fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
    1.25 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
    1.26 +fun error scan xs = scan xs handle ABORT msg => Output.error msg;
    1.27  
    1.28  
    1.29  (* finite scans *)