diff -r 8f4b72f0c15d -r 9e74cf11e4a4 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Thu Jul 02 16:53:55 1998 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Thu Jul 02 17:26:47 1998 +0200
@@ -146,7 +146,7 @@
   in
     (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))))
+    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
   end;