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 *)