1.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML Sat Jul 23 16:12:12 2011 +0200
1.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Sat Jul 23 16:37:17 2011 +0200
1.3 @@ -194,9 +194,9 @@
1.4 fun get_pos [] = " (past end-of-text!)"
1.5 | get_pos ((_, pos) :: _) = Position.str_of pos;
1.6
1.7 - fun err (syms, msg) =
1.8 + fun err (syms, msg) = fn () =>
1.9 text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
1.10 - (case msg of NONE => "" | SOME s => "\n" ^ s);
1.11 + (case msg of NONE => "" | SOME m => "\n" ^ m ());
1.12 in Scan.!! err scan end;
1.13
1.14 val any_line' =