| changeset 5112 | 9e74cf11e4a4 |
| parent 4938 | c8bbbf3c59fa |
| child 5910 | 151ee1a5c09c |
--- 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;