src/Provers/classical.ML
changeset 33522 737589bb9bb8
parent 33519 e31a85f92ce9
child 35613 9d3ff36ad4e1
     1.1 --- a/src/Provers/classical.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -835,13 +835,12 @@
     1.4  
     1.5  (* global clasets *)
     1.6  
     1.7 -structure GlobalClaset = TheoryDataFun
     1.8 +structure GlobalClaset = Theory_Data
     1.9  (
    1.10    type T = claset * context_cs;
    1.11    val empty = (empty_cs, empty_context_cs);
    1.12 -  val copy = I;
    1.13    val extend = I;
    1.14 -  fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
    1.15 +  fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
    1.16      (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
    1.17  );
    1.18