changeset 14825 | 8cdf5a813cec |
parent 14774 | d747c32e85e1 |
child 14981 | e73f8140af78 |
--- a/src/Pure/Thy/thy_info.ML Sat May 29 15:00:52 2004 +0200 +++ b/src/Pure/Thy/thy_info.ML Sat May 29 15:01:36 2004 +0200 @@ -341,7 +341,7 @@ ((case new_deps of Some deps => change_thys (update_node name parents (deps, thy)) | None => ()); - load_thy really ml (time orelse ! Library.timing) initiators dir name parents; + load_thy really ml (time orelse ! Output.timing) initiators dir name parents; false); in (visited', (result, name)) end end;