read: explicit treatment of scanner failure;
authorwenzelm
Thu, 27 Sep 2007 11:46:05 +0200
changeset 24739 e9f9d4297bda
parent 24738 258e1877d0c5
child 24740 36750aca7a77
read: explicit treatment of scanner failure;
src/Pure/Thy/thy_header.ML
--- 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