| changeset 48992 | 0518bf89c777 |
| parent 47005 | 421760a1efe7 |
| child 50201 | c26369c9eda6 |
--- a/src/Pure/consts.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/consts.ML Wed Aug 29 11:48:45 2012 +0200 @@ -146,7 +146,7 @@ fun read_const consts (raw_c, pos) = let val c = intern consts raw_c; - val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos); + val T = type_scheme consts c handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in Const (c, T) end;