# HG changeset patch
# User wenzelm
# Date 965130202 -7200
# Node ID c2606af9922c764cb8bb6a2601275e4dfd76add5
# Parent  aa757b35b129ab2a86a4ab9ba06f62965bab41b8
tuned msg;

diff -r aa757b35b129 -r c2606af9922c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 01 13:41:23 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 01 13:43:22 2000 +0200
@@ -262,12 +262,12 @@
 
 (* load_thy *)
 
-fun required_by [] = ""
-  | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
+fun required_by _ [] = ""
+  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
 fun load_thy ml time initiators dir name parents =
   let
-    val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
+    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val _ = touch_thy name;
     val master = ThyLoad.load_thy dir name ml time;
@@ -326,7 +326,7 @@
 
         val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
           error (loader_msg "the error(s) above occurred while examining theory" [name] ^
-            (if null initiators then "" else "\n" ^ required_by initiators));
+            (if null initiators then "" else required_by "\n" initiators));
         val (visited', parent_results) = foldl_map req_parent (name :: visited, parents);
 
         val result =