src/Pure/pure_thy.ML
changeset 18728 6790126ab5f6
parent 18713 cf777b9788b5
child 18778 f623f7a35ced
     1.1 --- a/src/Pure/pure_thy.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -47,35 +47,30 @@
     1.4    val thms_of: theory -> (string * thm) list
     1.5    val all_thms_of: theory -> (string * thm) list
     1.6    val hide_thms: bool -> string list -> theory -> theory
     1.7 -  val store_thm: (bstring * thm) * theory attribute list -> theory -> thm * theory
     1.8 +  val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
     1.9    val smart_store_thms: (bstring * thm list) -> thm list
    1.10    val smart_store_thms_open: (bstring * thm list) -> thm list
    1.11    val forall_elim_var: int -> thm -> thm
    1.12    val forall_elim_vars: int -> thm -> thm
    1.13 -  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> thm list * theory
    1.14 -  val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
    1.15 -    -> thm list list * theory 
    1.16 -  val note_thmss: theory attribute -> ((bstring * theory attribute list) *
    1.17 -    (thmref * theory attribute list) list) list ->
    1.18 -    theory -> (bstring * thm list) list * theory
    1.19 -  val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
    1.20 -    (thm list * theory attribute list) list) list ->
    1.21 -    theory -> (bstring * thm list) list * theory
    1.22 -  val add_axioms: ((bstring * string) * theory attribute list) list ->
    1.23 +  val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
    1.24 +  val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory 
    1.25 +  val note_thmss: attribute -> ((bstring * attribute list) *
    1.26 +    (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
    1.27 +  val note_thmss_i: attribute -> ((bstring * attribute list) *
    1.28 +    (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
    1.29 +  val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
    1.30 +  val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
    1.31 +  val add_axiomss: ((bstring * string list) * attribute list) list ->
    1.32 +    theory -> thm list list * theory
    1.33 +  val add_axiomss_i: ((bstring * term list) * attribute list) list ->
    1.34 +    theory -> thm list list * theory
    1.35 +  val add_defs: bool -> ((bstring * string) * attribute list) list ->
    1.36      theory -> thm list * theory
    1.37 -  val add_axioms_i: ((bstring * term) * theory attribute list) list ->
    1.38 +  val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
    1.39      theory -> thm list * theory
    1.40 -  val add_axiomss: ((bstring * string list) * theory attribute list) list ->
    1.41 -    theory -> thm list list * theory
    1.42 -  val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
    1.43 +  val add_defss: bool -> ((bstring * string list) * attribute list) list ->
    1.44      theory -> thm list list * theory
    1.45 -  val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
    1.46 -    theory -> thm list * theory
    1.47 -  val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
    1.48 -    theory -> thm list * theory
    1.49 -  val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
    1.50 -    theory -> thm list list * theory
    1.51 -  val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
    1.52 +  val add_defss_i: bool -> ((bstring * term list) * attribute list) list ->
    1.53      theory -> thm list list * theory
    1.54    val generic_setup: string option -> theory -> theory
    1.55    val add_oracle: bstring * string * string -> theory -> theory
    1.56 @@ -340,8 +335,7 @@
    1.57  (* add_thms(s) *)
    1.58  
    1.59  fun add_thms_atts pre_name ((bname, thms), atts) =
    1.60 -  enter_thms pre_name (name_thms false)
    1.61 -    (Thm.applys_attributes atts) (bname, thms);
    1.62 +  enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms);
    1.63  
    1.64  fun gen_add_thmss pre_name =
    1.65    fold_map (add_thms_atts pre_name);
    1.66 @@ -359,7 +353,7 @@
    1.67  
    1.68  fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
    1.69    let
    1.70 -    fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
    1.71 +    fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
    1.72      val (thms, thy') = thy |> enter_thms
    1.73        name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
    1.74        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);