# HG changeset patch
# User wenzelm
# Date 1280864078 -7200
# Node ID 8a2bacb8ad87c67cb189e7e9e69f90e032b2ed6b
# Parent  05691ad7407976d0dca6ee46304e94f1990b49c1
removed unused Update_Time data (cf. ac94ff28e9e1);

diff -r 05691ad74079 -r 8a2bacb8ad87 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;