tuned recover;
authorwenzelm
Mon, 03 Apr 2000 21:05:07 +0200
changeset 8663 38d7ec8ef683
parent 8662 f9679ddbc492
child 8664 aa383eeb3359
tuned recover;
src/Pure/General/symbol.ML
src/Pure/Isar/outer_lex.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;
--- 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))