1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 19:39:29 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 21:54:58 2000 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4   (if time then
     1.5      timeit (fn () =>
     1.6       (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
     1.7 -      setmp Library.timing true (run_thy name) path;
     1.8 +      run_thy name path;
     1.9        writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
    1.10    else run_thy name path;
    1.11    Context.context (ThyInfo.get_theory name);

     2.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jun 04 19:39:29 2000 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jun 04 21:54:58 2000 +0200
     2.3 @@ -246,7 +246,7 @@
     2.4      let val name = Path.pack path in
     2.5        timeit (fn () =>
     2.6         (writeln ("\n**** Starting file " ^ quote name ^ " ****");
     2.7 -        setmp Library.timing true run_file path;
     2.8 +        run_file path;
     2.9          writeln ("**** Finished file " ^ quote name ^ " ****\n")))
    2.10      end
    2.11    else run_file path;
    2.12 @@ -307,11 +307,10 @@
    2.13                end)
    2.14        end);
    2.15  
    2.16 -fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
    2.17 +fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
    2.18    let
    2.19      val path = Path.expand (Path.unpack str);
    2.20      val name = Path.pack (Path.base path);
    2.21 -    val time = time_arg orelse ! Library.timing;
    2.22    in
    2.23      if name mem_string initiators then error (cycle_msg name initiators) else ();
    2.24      if known_thy name andalso is_finished name orelse name mem_string visited then
    2.25 @@ -333,7 +332,7 @@
    2.26              ((case new_deps of
    2.27                Some deps => change_thys (update_node name parents (deps, None))
    2.28              | None => ());
    2.29 -             load_thy ml time initiators dir name parents;
    2.30 +             load_thy ml (time orelse ! Library.timing) initiators dir name parents;
    2.31               false);
    2.32        in (visited', (result, name)) end
    2.33    end;