1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 18:52:42 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 21:34:38 2010 +0200
     1.3 @@ -133,17 +133,6 @@
     1.4  
     1.5  (** thy operations **)
     1.6  
     1.7 -(* abstract update time *)
     1.8 -
     1.9 -structure Update_Time = Theory_Data
    1.10 -(
    1.11 -  type T = int;
    1.12 -  val empty = 0;
    1.13 -  fun extend _ = empty;
    1.14 -  fun merge _ = empty;
    1.15 -);
    1.16 -
    1.17 -
    1.18  (* remove theory *)
    1.19  
    1.20  fun remove_thy name =
    1.21 @@ -246,8 +235,7 @@
    1.22      val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
    1.23      fun init () =
    1.24        Thy_Load.begin_theory dir name parent_thys uses
    1.25 -      |> Present.begin_theory update_time dir uses
    1.26 -      |> Update_Time.put update_time;
    1.27 +      |> Present.begin_theory update_time dir uses;
    1.28  
    1.29      val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
    1.30