1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -331,18 +331,19 @@
     1.4  
     1.5  fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
     1.6  
     1.7 -fun scan_err msg [] = "Boogie (at end of input): " ^ msg
     1.8 -  | scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^
     1.9 -      msg
    1.10 +fun scan_err msg [] = (fn () => "Boogie (at end of input): " ^ msg ())
    1.11 +  | scan_err msg ((i, _) :: _) =
    1.12 +      (fn () => "Boogie (at line " ^ string_of_int i ^ "): " ^ msg ())
    1.13  
    1.14 -fun scan_fail msg = Scan.fail_with (scan_err msg)
    1.15 +fun scan_fail' msg = Scan.fail_with (scan_err msg)
    1.16 +fun scan_fail s = scan_fail' (fn () => s)
    1.17  
    1.18  fun finite scan fold_lines input =
    1.19    let val (i, ts) = tokenize fold_lines input
    1.20    in
    1.21      (case Scan.error (Scan.finite (stopper i) scan) ts of
    1.22        (x, []) => x
    1.23 -    | (_, ts') => error (scan_err "unparsed input" ts'))
    1.24 +    | (_, ts') => error ((scan_err (fn () => "unparsed input") ts') ()))
    1.25    end
    1.26  
    1.27  fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
    1.28 @@ -361,7 +362,7 @@
    1.29  fun scan_lookup kind tab key =
    1.30    (case Symtab.lookup tab key of
    1.31      SOME value => Scan.succeed value
    1.32 -  | NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key))
    1.33 +  | NONE => scan_fail' (fn () => "undefined " ^ kind ^ ": " ^ quote key))
    1.34  
    1.35  fun typ tds =
    1.36    let