src/Pure/Thy/thy_info.ML
changeset 48992 0518bf89c777
parent 48928 698fb0e27b11
child 49010 72808e956879
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -274,7 +274,7 @@
           val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
-                Position.str_of require_pos ^ required_by "\n" initiators);
+                Position.here require_pos ^ required_by "\n" initiators);
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =