src/Provers/classical.ML
changeset 22846 fb79144af9a3
parent 22674 1a610904bbca
child 23178 07ba6b58b3d2
     1.1 --- a/src/Provers/classical.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -140,9 +140,9 @@
     1.4    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
     1.5    val del_context_unsafe_wrapper: string -> theory -> theory
     1.6    val get_claset: theory -> claset
     1.7 -  val print_local_claset: Proof.context -> unit
     1.8    val get_local_claset: Proof.context -> claset
     1.9    val put_local_claset: claset -> Proof.context -> Proof.context
    1.10 +  val print_local_claset: Proof.context -> unit
    1.11    val safe_dest: int option -> attribute
    1.12    val safe_elim: int option -> attribute
    1.13    val safe_intro: int option -> attribute
    1.14 @@ -857,19 +857,16 @@
    1.15  (* global claset *)
    1.16  
    1.17  structure GlobalClaset = TheoryDataFun
    1.18 -(struct
    1.19 -  val name = "Provers/claset";
    1.20 +(
    1.21    type T = claset ref * context_cs;
    1.22 -
    1.23    val empty = (ref empty_cs, empty_context_cs);
    1.24    fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
    1.25    val extend = copy;
    1.26    fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
    1.27      (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
    1.28 -  fun print _ (ref cs, _) = print_cs cs;
    1.29 -end);
    1.30 +);
    1.31  
    1.32 -val print_claset = GlobalClaset.print;
    1.33 +val print_claset = print_cs o ! o #1 o GlobalClaset.get;
    1.34  val get_claset = ! o #1 o GlobalClaset.get;
    1.35  
    1.36  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    1.37 @@ -912,20 +909,19 @@
    1.38  (* local claset *)
    1.39  
    1.40  structure LocalClaset = ProofDataFun
    1.41 -(struct
    1.42 -  val name = "Provers/claset";
    1.43 +(
    1.44    type T = claset;
    1.45    val init = get_claset;
    1.46 -  fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
    1.47 -end);
    1.48 +);
    1.49  
    1.50 -val print_local_claset = LocalClaset.print;
    1.51  val get_local_claset = LocalClaset.get;
    1.52  val put_local_claset = LocalClaset.put;
    1.53  
    1.54  fun local_claset_of ctxt =
    1.55    context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
    1.56  
    1.57 +val print_local_claset = print_cs o local_claset_of;
    1.58 +
    1.59  
    1.60  (* attributes *)
    1.61  
    1.62 @@ -1061,7 +1057,7 @@
    1.63  
    1.64  (** theory setup **)
    1.65  
    1.66 -val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
    1.67 +val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
    1.68  
    1.69  
    1.70