error "Unexpected end of input";

--- 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 *)