src/Sequents/prover.ML
changeset 16458 4c6fd0c01d28
parent 13105 3d1e7a199bdc
child 18708 4b3dadb4fe33
     1.1 --- a/src/Sequents/prover.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Sequents/prover.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -168,32 +168,27 @@
     1.4  
     1.5  
     1.6  
     1.7 -structure ProverArgs =
     1.8 -  struct
     1.9 +structure ProverData = TheoryDataFun
    1.10 +(struct
    1.11    val name = "Sequents/prover";
    1.12    type T = pack ref;
    1.13    val empty = ref empty_pack
    1.14    fun copy (ref pack) = ref pack;
    1.15 -  val prep_ext = copy;
    1.16 -  fun merge (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
    1.17 +  val extend = copy;
    1.18 +  fun merge _ (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
    1.19    fun print _ (ref pack) = print_pack pack;
    1.20 -  end;
    1.21 -
    1.22 -structure ProverData = TheoryDataFun(ProverArgs);
    1.23 +end);
    1.24  
    1.25  val prover_setup = [ProverData.init];
    1.26  
    1.27  val print_pack = ProverData.print;
    1.28 -val pack_ref_of_sg = ProverData.get_sg;
    1.29  val pack_ref_of = ProverData.get;
    1.30  
    1.31  (* access global pack *)
    1.32  
    1.33 -val pack_of_sg = ! o pack_ref_of_sg;
    1.34 -val pack_of = pack_of_sg o sign_of;
    1.35 -
    1.36 +val pack_of = ! o pack_ref_of;
    1.37  val pack = pack_of o Context.the_context;
    1.38 -val pack_ref = pack_ref_of_sg o sign_of o Context.the_context;
    1.39 +val pack_ref = pack_ref_of o Context.the_context;
    1.40  
    1.41  
    1.42  (* change global pack *)