--- a/src/HOL/SPARK/Tools/fdl_parser.ML Sat Jul 23 16:12:12 2011 +0200
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML Sat Jul 23 16:37:17 2011 +0200
@@ -72,10 +72,10 @@
fun get_pos [] = " (past end-of-file!)"
| get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
- fun err (syms, msg) =
+ fun err (syms, msg) = fn () =>
"Syntax error" ^ get_pos syms ^ " at " ^
- beginning 10 (map Fdl_Lexer.unparse syms) ^
- (case msg of NONE => "" | SOME s => "\n" ^ s ^ " expected");
+ beginning 10 (map Fdl_Lexer.unparse syms) ^
+ (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected");
in Scan.!! err scan end;
fun parse_all p =
@@ -84,7 +84,7 @@
(** parsers **)
-fun group s p = p || Scan.fail_with (K s);
+fun group s p = p || Scan.fail_with (K (fn () => s));
fun $$$ s = group s
(Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso