author | wenzelm |
Thu, 27 Sep 2007 11:46:05 +0200 | |
changeset 24739 | e9f9d4297bda |
parent 24738 | 258e1877d0c5 |
child 24740 | 36750aca7a77 |
--- a/src/Pure/Thy/thy_header.ML Wed Sep 26 22:38:11 2007 +0200 +++ b/src/Pure/Thy/thy_header.ML Thu Sep 27 11:46:05 2007 +0200 @@ -54,7 +54,7 @@ |> Symbol.source false |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos |> T.source_proper - |> Source.source T.stopper (Scan.single (Scan.error header)) NONE + |> Source.source T.stopper (Scan.single (Scan.error (P.!!! header))) NONE |> Source.get_single; in (case res of SOME (x, _) => x