changeset 48992 | 0518bf89c777 |
parent 47021 | f35f654f297d |
child 49358 | 0fa351b1bd14 |
--- a/src/Pure/General/name_space.ML Wed Aug 29 11:31:07 2012 +0200 +++ b/src/Pure/General/name_space.ML Wed Aug 29 11:48:45 2012 +0200 @@ -424,7 +424,7 @@ let val name = intern space xname in (case Symtab.lookup tab name of SOME x => (Context_Position.report_generic context pos (markup space name); (name, x)) - | NONE => error (undefined (kind_of space) name ^ Position.str_of pos)) + | NONE => error (undefined (kind_of space) name ^ Position.here pos)) end; fun get (space, tab) name =