diff -r c9c481bc0216 -r c68a9c510c90 src/Pure/Syntax/scan.ML
--- a/src/Pure/Syntax/scan.ML	Tue May 26 12:29:10 1998 +0200
+++ b/src/Pure/Syntax/scan.ML	Tue May 26 12:29:27 1998 +0200
@@ -189,7 +189,7 @@
 
 fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
   let
-    val drain_with = drain def_prmpt get stopper;
+    fun drain_with scan = drain def_prmpt get stopper scan;
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>