removed unused Update_Time data (cf. ac94ff28e9e1);
--- 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;