src/Pure/General/name_space.ML
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 =