--- a/src/Pure/General/symbol.ML Mon Apr 03 14:02:40 2000 +0200
+++ b/src/Pure/General/symbol.ML Mon Apr 03 21:05:07 2000 +0200
@@ -275,7 +275,7 @@
(* source *)
-val recover = Scan.any1 ((not o is_blank) andf not_eof);
+val recover = Scan.any ((not o is_blank) andf not_eof);
fun source do_recover src =
Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
--- a/src/Pure/Isar/outer_lex.ML Mon Apr 03 14:02:40 2000 +0200
+++ b/src/Pure/Isar/outer_lex.ML Mon Apr 03 21:05:07 2000 +0200
@@ -247,7 +247,7 @@
(* source of (proper) tokens *)
val is_junk = (not o Symbol.is_blank) andf Symbol.not_sync andf Symbol.not_eof;
-fun recover xs = keep_line (Scan.any1 is_junk) xs;
+fun recover xs = keep_line (Scan.any is_junk) xs;
fun source do_recover get_lex pos src =
Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))