have_thmss: handle multiple lists of arguments;
authorwenzelm
Thu Jun 29 22:29:46 2000 +0200 (2000-06-29)
changeset 9192df32cd0881b9
parent 9191 300bd596d696
child 9193 4f4936582889
have_thmss: handle multiple lists of arguments;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Thu Jun 29 16:50:52 2000 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Jun 29 22:29:46 2000 +0200
     1.3 @@ -32,8 +32,8 @@
     1.4    val forall_elim_vars: int -> thm -> thm
     1.5    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
     1.6    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list
     1.7 -  val have_thmss: bstring -> theory attribute list ->
     1.8 -    (thm list * theory attribute list) list -> theory -> theory * thm list
     1.9 +  val have_thmss: theory attribute list -> ((bstring * theory attribute list) *
    1.10 +    (thm list * theory attribute list) list) list -> theory -> theory * (string * thm list) list
    1.11    val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
    1.12    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
    1.13    val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
    1.14 @@ -248,14 +248,18 @@
    1.15  
    1.16  (* have_thmss *)
    1.17  
    1.18 -fun have_thmss bname more_atts ths_atts thy =
    1.19 -  let
    1.20 -    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
    1.21 -    val (thy', thmss') =
    1.22 -      foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts);
    1.23 -    val thms' = flat thmss';
    1.24 -    val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, thms');
    1.25 -  in (thy', thms'') end;
    1.26 +local
    1.27 +  fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) =
    1.28 +    let
    1.29 +      fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
    1.30 +      val (thy', thmss') =
    1.31 +        foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts @ kind_atts)) ths_atts);
    1.32 +      val thms' = flat thmss';
    1.33 +      val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, thms');
    1.34 +    in (thy', (bname, thms'')) end;
    1.35 +in
    1.36 +  fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args);
    1.37 +end;
    1.38  
    1.39  
    1.40  (* store_thm *)