src/Pure/General/symbol.ML
changeset 43947 9b00f09f7721
parent 43845 d89353d17f54
child 47850 c638127b4653
     1.1 --- a/src/Pure/General/symbol.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -404,13 +404,13 @@
     1.4  
     1.5  fun scanner msg scan chs =
     1.6    let
     1.7 -    fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs)
     1.8 -      | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
     1.9 +    fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))
    1.10 +      | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));
    1.11      val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
    1.12    in
    1.13      (case fin_scan chs of
    1.14        (result, []) => result
    1.15 -    | (_, rest) => error (message (rest, NONE)))
    1.16 +    | (_, rest) => error (message (rest, NONE) ()))
    1.17    end;
    1.18  
    1.19  val scan_id = Scan.one is_letter ^^ (Scan.many is_letdig >> implode);