src/Pure/raw_simplifier.ML
changeset 48992 0518bf89c777
parent 47239 0b1829860149
child 49660 de49d9b4d7bc
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Aug 29 11:31:07 2012 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Aug 29 11:48:45 2012 +0200
     1.3 @@ -1057,7 +1057,7 @@
     1.4                   val _ =
     1.5                     if b <> b' then
     1.6                       warning ("Simplifier: renamed bound variable " ^
     1.7 -                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
     1.8 +                       quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
     1.9                     else ();
    1.10                   val ss' = add_bound ((b', T), a) ss;
    1.11                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;