src/Pure/Thy/thy_scan.ML

   let
     val chs = explode str;	(*sic!*)
     val scan_toks = Scan.repeat (scan_token lex);
     val ignore = fn (Ignore, _, _) => true | _ => false;
   in
-    (case Scan.error (Scan.finite' Symbol.eof scan_toks) (Some 1, chs) of
+    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
     | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (beginning cs))))
   end;