1.1 --- a/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -72,10 +72,10 @@
     1.4      fun get_pos [] = " (past end-of-file!)"
     1.5        | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
     1.6  
     1.7 -    fun err (syms, msg) =
     1.8 +    fun err (syms, msg) = fn () =>
     1.9        "Syntax error" ^ get_pos syms ^ " at " ^
    1.10 -      beginning 10 (map Fdl_Lexer.unparse syms) ^
    1.11 -      (case msg of NONE => "" | SOME s => "\n" ^ s ^ " expected");
    1.12 +        beginning 10 (map Fdl_Lexer.unparse syms) ^
    1.13 +        (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected");
    1.14    in Scan.!! err scan end;
    1.15  
    1.16  fun parse_all p =
    1.17 @@ -84,7 +84,7 @@
    1.18  
    1.19  (** parsers **)
    1.20  
    1.21 -fun group s p = p || Scan.fail_with (K s);
    1.22 +fun group s p = p || Scan.fail_with (K (fn () => s));
    1.23  
    1.24  fun $$$ s = group s
    1.25    (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso