src/HOL/SPARK/Tools/fdl_lexer.ML
changeset 43947 9b00f09f7721
parent 41584 2b07a4212d6d
child 47083 d04b38d4035b
     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' =