--- a/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:42 2009 +0100
@@ -233,15 +233,14 @@
(* management data *)
-structure Management_Data = TheoryDataFun
+structure Management_Data = Theory_Data
(
type T =
Task_Queue.group option * (*worker thread group*)
int; (*abstract update time*)
val empty = (NONE, 0);
- val copy = I;
fun extend _ = empty;
- fun merge _ _ = empty;
+ fun merge _ = empty;
);
val thy_ord = int_ord o pairself (#2 o Management_Data.get);