src/Pure/section_utils.ML

--- a/src/Pure/section_utils.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/section_utils.ML	Mon May 18 17:57:47 1998 +0200
@@ -34,7 +34,7 @@
 (*Skipping initial blanks, find the first identifier*)	(* FIXME *)
 fun scan_to_id s = 
     s |> Symbol.explode
-    |> Scan.error (Scan.finite Symbol.eof
+    |> Scan.error (Scan.finite Symbol.stopper
       (!! (fn _ => "Expected to find an identifier in " ^ s)
         (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
     |> #1;