added get_cs/map_cs;
authorwenzelm
Sat Jul 28 20:40:26 2007 +0200 (2007-07-28)
changeset 24021491c68f40bc4
parent 24020 ed4d7abffee7
child 24022 ab76c73b3b58
added get_cs/map_cs;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Sat Jul 28 20:40:24 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Jul 28 20:40:26 2007 +0200
     1.3 @@ -143,6 +143,8 @@
     1.4    val get_local_claset: Proof.context -> claset
     1.5    val put_local_claset: claset -> Proof.context -> Proof.context
     1.6    val print_local_claset: Proof.context -> unit
     1.7 +  val get_cs: Context.generic -> claset
     1.8 +  val map_cs: (claset -> claset) -> Context.generic -> Context.generic
     1.9    val safe_dest: int option -> attribute
    1.10    val safe_elim: int option -> attribute
    1.11    val safe_intro: int option -> attribute
    1.12 @@ -860,7 +862,7 @@
    1.13  
    1.14  (** claset data **)
    1.15  
    1.16 -(* global claset *)
    1.17 +(* global clasets *)
    1.18  
    1.19  structure GlobalClaset = TheoryDataFun
    1.20  (
    1.21 @@ -912,7 +914,7 @@
    1.22    (AList.delete (op =) name);
    1.23  
    1.24  
    1.25 -(* local claset *)
    1.26 +(* local clasets *)
    1.27  
    1.28  structure LocalClaset = ProofDataFun
    1.29  (
    1.30 @@ -929,6 +931,15 @@
    1.31  val print_local_claset = print_cs o local_claset_of;
    1.32  
    1.33  
    1.34 +(* generic clasets *)
    1.35 +
    1.36 +fun get_cs (Context.Theory thy) = claset_of thy
    1.37 +  | get_cs (Context.Proof ctxt) = local_claset_of ctxt;
    1.38 +
    1.39 +fun map_cs f (Context.Theory thy) = (change_claset_of thy f; Context.Theory thy)
    1.40 +  | map_cs f (Context.Proof ctxt) = Context.Proof (LocalClaset.map f ctxt);
    1.41 +
    1.42 +
    1.43  (* attributes *)
    1.44  
    1.45  fun attrib f = Thm.declaration_attribute (fn th =>