# HG changeset patch
# User wenzelm
# Date 1011801525 -3600
# Node ID c7066d8b684f2d223ce1325ed7268513228de566
# Parent  584a3e0b00f2fea16b819a7d684cf68b4e5b34ce
error "Unexpected end of input";

diff -r 584a3e0b00f2 -r c7066d8b684f src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Wed Jan 23 16:58:26 2002 +0100
+++ b/src/Pure/Isar/thy_header.ML	Wed Jan 23 16:58:45 2002 +0100
@@ -24,12 +24,17 @@
 (* scan header *)
 
 fun scan_header get_lex scan (src, pos) =
-  src
-  |> Symbol.source false
-  |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
-  |> T.source_proper
-  |> Source.source T.stopper (Scan.single scan) None
-  |> (fst o the o Source.get_single);
+  let val res =
+    src
+    |> Symbol.source false
+    |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
+    |> T.source_proper
+    |> Source.source T.stopper (Scan.single scan) None
+    |> Source.get_single;
+  in
+    (case res of Some (x, _) => x
+    | None => error ("Unexpected end of input" ^ Position.str_of pos))
+  end;
 
 
 (* keywords *)