src/HOL/SPARK/Tools/fdl_lexer.ML

 
 val long_identifier =
   identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat);
 
 val whitespace = Scan.many (is_whitespace o symbol);
+val whitespace1 = Scan.many1 (is_whitespace o symbol);
 val whitespace' = Scan.many (is_whitespace' o symbol);
 val newline = Scan.one (is_newline o symbol);
 
 fun beginning n cs =
   let

 fun scan header comment =
   !!! "bad header" header --| whitespace --
   Scan.repeat (Scan.unless (Scan.one is_char_eof)
     (!!! "bad input"
        (   comment
-        || (keyword "For" -- whitespace) |--
+        || (keyword "For" -- whitespace1) |--
               Scan.repeat1 (Scan.unless (keyword ":") any) --|
               keyword ":" >> make_token Traceability
         || Scan.max leq_token
              (Scan.literal lexicon >> make_token Keyword)
              (   long_identifier >> make_token Long_Ident