src/Pure/Thy/thy_scan.ML
changeset 5112 9e74cf11e4a4
parent 4938 c8bbbf3c59fa
child 5910 151ee1a5c09c
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Thu Jul 02 16:53:55 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Thu Jul 02 17:26:47 1998 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4    in
     1.5      (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
     1.6        (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
     1.7 -    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (beginning cs))))
     1.8 +    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
     1.9    end;
    1.10  
    1.11