src/Pure/section_utils.ML
changeset 4938 c8bbbf3c59fa
parent 4848 99c8d95c51d6
child 6039 01f67f5f8dd0
     1.1 --- a/src/Pure/section_utils.ML	Mon May 18 17:57:16 1998 +0200
     1.2 +++ b/src/Pure/section_utils.ML	Mon May 18 17:57:47 1998 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  (*Skipping initial blanks, find the first identifier*)	(* FIXME *)
     1.5  fun scan_to_id s = 
     1.6      s |> Symbol.explode
     1.7 -    |> Scan.error (Scan.finite Symbol.eof
     1.8 +    |> Scan.error (Scan.finite Symbol.stopper
     1.9        (!! (fn _ => "Expected to find an identifier in " ^ s)
    1.10          (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    1.11      |> #1;