--- a/src/Pure/Thy/thy_info.ML Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Jan 14 17:14:06 2006 +0100
@@ -356,9 +356,10 @@
val req_parent = require_thy true true time (strict andalso keep_strict) keep_strict
(name :: initiators);
- 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 required_by "\n" initiators));
+ val (current, (new_deps, parents)) = current_deps ml strict dir name
+ handle ERROR msg => cat_error msg
+ (loader_msg "the error(s) above occurred while examining theory" [name] ^
+ (if null initiators then "" else required_by "\n" initiators));
val dir' = if_none (opt_path'' new_deps) dir;
val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);