removed unused Update_Time data (cf. ac94ff28e9e1);
authorwenzelm
Tue, 03 Aug 2010 21:34:38 +0200
changeset 38141 8a2bacb8ad87
parent 38140 05691ad74079
child 38142 c202426474c3
removed unused Update_Time data (cf. ac94ff28e9e1);
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 18:52:42 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 21:34:38 2010 +0200
@@ -133,17 +133,6 @@
 
 (** thy operations **)
 
-(* abstract update time *)
-
-structure Update_Time = Theory_Data
-(
-  type T = int;
-  val empty = 0;
-  fun extend _ = empty;
-  fun merge _ = empty;
-);
-
-
 (* remove theory *)
 
 fun remove_thy name =
@@ -246,8 +235,7 @@
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init () =
       Thy_Load.begin_theory dir name parent_thys uses
-      |> Present.begin_theory update_time dir uses
-      |> Update_Time.put update_time;
+      |> Present.begin_theory update_time dir uses;
 
     val (after_load, theory) = Outer_Syntax.load_thy name init pos text;