src/Pure/global_theory.ML

       | name => name);
     val res = Facts.lookup context facts name;
     val _ = Theory.check_thy thy;
   in
     (case res of
-      NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
+      NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
     | SOME (static, ths) =>
         (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
          if static then ()
          else Context_Position.report_generic context pos (Isabelle_Markup.dynamic_fact name);
          Facts.select xthmref (map (Thm.transfer thy) ths)))