src/Pure/General/symbol_pos.ML
changeset 48992 0518bf89c777
parent 48911 5debc3e4fa81
child 50201 c26369c9eda6
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Aug 29 11:31:07 2012 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Aug 29 11:48:45 2012 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  fun !!! text scan =
     1.5    let
     1.6      fun get_pos [] = " (end-of-input)"
     1.7 -      | get_pos ((_, pos) :: _) = Position.str_of pos;
     1.8 +      | get_pos ((_, pos) :: _) = Position.here pos;
     1.9  
    1.10      fun err (syms, msg) = fn () =>
    1.11        text () ^ get_pos syms ^