# HG changeset patch
# User wenzelm
# Date 954788707 -7200
# Node ID 38d7ec8ef683095f3769d1bcf5afba3eaacc9478
# Parent  f9679ddbc492a917287b138152a7208989972d46
tuned recover;

diff -r f9679ddbc492 -r 38d7ec8ef683 src/Pure/General/symbol.ML
--- 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;
diff -r f9679ddbc492 -r 38d7ec8ef683 src/Pure/Isar/outer_lex.ML
--- 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))