--- a/src/Pure/General/scan.ML Wed May 12 16:51:52 1999 +0200
+++ b/src/Pure/General/scan.ML Wed May 12 16:52:28 1999 +0200
@@ -193,7 +193,6 @@
| _ => None);
-
(* infinite scans -- draining state-based source *)
fun drain def_prmpt get stopper scan ((state, xs), src) =