src/Provers/classical.ML
changeset 32261 05e687ddbcee
parent 32148 253f6808dabe
child 32740 9dd0a2f83429
     1.1 --- a/src/Provers/classical.ML	Tue Jul 28 20:03:58 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Jul 29 00:09:14 2009 +0200
     1.3 @@ -113,8 +113,8 @@
     1.4    val del_context_safe_wrapper: string -> theory -> theory
     1.5    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
     1.6    val del_context_unsafe_wrapper: string -> theory -> theory
     1.7 -  val get_claset: theory -> claset
     1.8 -  val map_claset: (claset -> claset) -> theory -> theory
     1.9 +  val get_claset: Proof.context -> claset
    1.10 +  val put_claset: claset -> Proof.context -> Proof.context
    1.11    val get_cs: Context.generic -> claset
    1.12    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    1.13    val safe_dest: int option -> attribute
    1.14 @@ -845,8 +845,8 @@
    1.15      (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
    1.16  );
    1.17  
    1.18 -val get_claset = #1 o GlobalClaset.get;
    1.19 -val map_claset = GlobalClaset.map o apfst;
    1.20 +val get_global_claset = #1 o GlobalClaset.get;
    1.21 +val map_global_claset = GlobalClaset.map o apfst;
    1.22  
    1.23  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    1.24  fun map_context_cs f = GlobalClaset.map (apsnd
    1.25 @@ -871,9 +871,12 @@
    1.26  structure LocalClaset = ProofDataFun
    1.27  (
    1.28    type T = claset;
    1.29 -  val init = get_claset;
    1.30 +  val init = get_global_claset;
    1.31  );
    1.32  
    1.33 +val get_claset = LocalClaset.get;
    1.34 +val put_claset = LocalClaset.put;
    1.35 +
    1.36  fun claset_of ctxt =
    1.37    context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
    1.38  
    1.39 @@ -881,13 +884,13 @@
    1.40  (* generic clasets *)
    1.41  
    1.42  val get_cs = Context.cases global_claset_of claset_of;
    1.43 -fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
    1.44 +fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
    1.45  
    1.46  
    1.47  (* attributes *)
    1.48  
    1.49  fun attrib f = Thm.declaration_attribute (fn th =>
    1.50 -  Context.mapping (map_claset (f th)) (LocalClaset.map (f th)));
    1.51 +  Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
    1.52  
    1.53  fun safe_dest w = attrib (addSE w o make_elim);
    1.54  val safe_elim = attrib o addSE;