# HG changeset patch
# User wenzelm
# Date 1386851003 -3600
# Node ID 5f5608bfe2307619ba4e299f8766ecfe1d6765ea
# Parent  0a9920e46b3a259df85fc840514b95e53ec7334c
tuned message;

diff -r 0a9920e46b3a -r 5f5608bfe230 src/Pure/Thy/thy_info.ML
--- 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;
diff -r 0a9920e46b3a -r 5f5608bfe230 src/Pure/Thy/thy_info.scala
--- 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))