removed old global get_claset/map_claset;
authorwenzelm
Wed Jul 29 00:09:14 2009 +0200 (2009-07-29)
changeset 3226105e687ddbcee
parent 32260 eb97888fa422
child 32262 73cd8f74cf2a
removed old global get_claset/map_claset;
added local get_claset/put_claset;
src/FOL/FOL.thy
src/FOL/cladata.ML
src/Provers/classical.ML
     1.1 --- a/src/FOL/FOL.thy	Tue Jul 28 20:03:58 2009 +0200
     1.2 +++ b/src/FOL/FOL.thy	Wed Jul 29 00:09:14 2009 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  use "cladata.ML"
     1.6  setup Cla.setup
     1.7 -setup cla_setup
     1.8 +ML {* Context.>> (Cla.map_cs (K FOL_cs)) *}
     1.9  
    1.10  ML {*
    1.11    structure Blast = Blast
     2.1 --- a/src/FOL/cladata.ML	Tue Jul 28 20:03:58 2009 +0200
     2.2 +++ b/src/FOL/cladata.ML	Wed Jul 29 00:09:14 2009 +0200
     2.3 @@ -32,4 +32,3 @@
     2.4  val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
     2.5                       addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
     2.6  
     2.7 -val cla_setup = Cla.map_claset (K FOL_cs);
     3.1 --- a/src/Provers/classical.ML	Tue Jul 28 20:03:58 2009 +0200
     3.2 +++ b/src/Provers/classical.ML	Wed Jul 29 00:09:14 2009 +0200
     3.3 @@ -113,8 +113,8 @@
     3.4    val del_context_safe_wrapper: string -> theory -> theory
     3.5    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
     3.6    val del_context_unsafe_wrapper: string -> theory -> theory
     3.7 -  val get_claset: theory -> claset
     3.8 -  val map_claset: (claset -> claset) -> theory -> theory
     3.9 +  val get_claset: Proof.context -> claset
    3.10 +  val put_claset: claset -> Proof.context -> Proof.context
    3.11    val get_cs: Context.generic -> claset
    3.12    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    3.13    val safe_dest: int option -> attribute
    3.14 @@ -845,8 +845,8 @@
    3.15      (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
    3.16  );
    3.17  
    3.18 -val get_claset = #1 o GlobalClaset.get;
    3.19 -val map_claset = GlobalClaset.map o apfst;
    3.20 +val get_global_claset = #1 o GlobalClaset.get;
    3.21 +val map_global_claset = GlobalClaset.map o apfst;
    3.22  
    3.23  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    3.24  fun map_context_cs f = GlobalClaset.map (apsnd
    3.25 @@ -871,9 +871,12 @@
    3.26  structure LocalClaset = ProofDataFun
    3.27  (
    3.28    type T = claset;
    3.29 -  val init = get_claset;
    3.30 +  val init = get_global_claset;
    3.31  );
    3.32  
    3.33 +val get_claset = LocalClaset.get;
    3.34 +val put_claset = LocalClaset.put;
    3.35 +
    3.36  fun claset_of ctxt =
    3.37    context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
    3.38  
    3.39 @@ -881,13 +884,13 @@
    3.40  (* generic clasets *)
    3.41  
    3.42  val get_cs = Context.cases global_claset_of claset_of;
    3.43 -fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
    3.44 +fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
    3.45  
    3.46  
    3.47  (* attributes *)
    3.48  
    3.49  fun attrib f = Thm.declaration_attribute (fn th =>
    3.50 -  Context.mapping (map_claset (f th)) (LocalClaset.map (f th)));
    3.51 +  Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
    3.52  
    3.53  fun safe_dest w = attrib (addSE w o make_elim);
    3.54  val safe_elim = attrib o addSE;