# HG changeset patch
# User wenzelm
# Date 1120639309 -7200
# Node ID ecca9fd2754f644dee761745f762872f9ed6c533
# Parent  d9e3ef66b38cf7cd0d7fec4b78a66a2a913ec294
ThyInfo.time_use root;

diff -r d9e3ef66b38c -r ecca9fd2754f src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed Jul 06 10:41:48 2005 +0200
+++ b/src/Pure/Isar/session.ML	Wed Jul 06 10:41:49 2005 +0200
@@ -79,7 +79,7 @@
       (init reset parent name;
        Present.init build info doc doc_graph (path ()) name
          (if dump = "" then NONE else SOME (Path.unpack dump)) (get_rpath rpath_str) verbose;
-       File.use (Path.basic root);
+       ThyInfo.time_use root;
        finish ())))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);