src/Pure/General/binding.ML
changeset 48992 0518bf89c777
parent 46897 ec793befc232
child 50201 c26369c9eda6
--- a/src/Pure/General/binding.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/General/binding.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -133,7 +133,7 @@
 
 (* check *)
 
-fun bad binding = "Bad name binding: " ^ print binding ^ Position.str_of (pos_of binding);
+fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
 
 fun check binding =
   if Symbol.is_ident (Symbol.explode (name_of binding)) then ()