diff -r b5eb7c688836 -r 740a0ca7e09b src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Sun Mar 15 19:48:49 2015 +0100 +++ b/src/Pure/Thy/thy_info.scala Sun Mar 15 20:35:47 2015 +0100 @@ -134,7 +134,7 @@ try { if (initiators.contains(name)) error(cycle_msg(initiators)) val header = - try { resources.check_thy(session, name).cat_errors(message) } + try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports) }