--- a/src/Provers/classical.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Provers/classical.ML Sun Nov 08 18:43:42 2009 +0100
@@ -835,13 +835,12 @@
(* global clasets *)
-structure GlobalClaset = TheoryDataFun
+structure GlobalClaset = Theory_Data
(
type T = claset * context_cs;
val empty = (empty_cs, empty_context_cs);
- val copy = I;
val extend = I;
- fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
+ fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
);