# HG changeset patch
# User wenzelm
# Date 978115560 -3600
# Node ID afdb47b973171141c15dc70a5b0588c8a5d14450
# Parent  74ed77fa5310f99380348af807418b9f95cddf93
recover: ignore result;

diff -r 74ed77fa5310 -r afdb47b97317 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Dec 29 19:45:33 2000 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Dec 29 19:46:00 2000 +0100
@@ -237,7 +237,7 @@
   let
     val no_terminator =
       Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
-    val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
+    val recover = Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None];
   in
     src
     |> Source.source T.stopper