--- a/src/Pure/Thy/thy_info.ML Wed Dec 11 17:30:51 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Dec 12 13:23:23 2013 +0100
@@ -328,7 +328,7 @@
val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
handle ERROR msg => cat_error msg
- (loader_msg "the error(s) above occurred while examining theory" [name] ^
+ (loader_msg "the error(s) above occurred for theory" [name] ^
Position.here require_pos ^ required_by "\n" initiators);
val parents = map (base_name o #1) imports;
--- a/src/Pure/Thy/thy_info.scala Wed Dec 11 17:30:51 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala Thu Dec 12 13:23:23 2013 +0100
@@ -89,8 +89,7 @@
else if (thy_load.loaded_theories(name.theory)) required + name
else {
def message: String =
- "The error(s) above occurred while examining theory " +
- quote(name.theory) + required_by(initiators)
+ "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators)
try {
if (initiators.contains(name)) error(cycle_msg(initiators))