removed obsolete add_axiomss(_i);
authorwenzelm
Thu Apr 03 23:38:59 2008 +0200 (2008-04-03)
changeset 26553748631e95425
parent 26552 5677b4faf295
child 26554 5ee45391576e
removed obsolete add_axiomss(_i);
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Thu Apr 03 22:21:29 2008 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 03 23:38:59 2008 +0200
     1.3 @@ -60,10 +60,6 @@
     1.4    val forall_elim_vars: int -> thm -> thm
     1.5    val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory
     1.6    val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> thm list * theory
     1.7 -  val add_axiomss: ((bstring * string list) * attribute list) list ->
     1.8 -    theory -> thm list list * theory
     1.9 -  val add_axiomss_i: ((bstring * term list) * attribute list) list ->
    1.10 -    theory -> thm list list * theory
    1.11    val add_defs: bool -> ((bstring * string) * attribute list) list ->
    1.12      theory -> thm list * theory
    1.13    val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
    1.14 @@ -362,29 +358,19 @@
    1.15  local
    1.16    fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
    1.17    fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs;
    1.18 -  fun add_single add ((name, ax), atts) thy =
    1.19 +  fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
    1.20      let
    1.21        val named_ax = [(name, ax)];
    1.22        val thy' = add named_ax thy;
    1.23        val thm = hd (get_axs thy' named_ax);
    1.24 -    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
    1.25 -  fun add_multi add ((name, axs), atts) thy =
    1.26 -    let
    1.27 -      val named_axs = name_multi name axs;
    1.28 -      val thy' = add named_axs thy;
    1.29 -      val thms = get_axs thy' named_axs;
    1.30 -    in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
    1.31 -  fun add_singles add = fold_map (add_single add);
    1.32 -  fun add_multis add = fold_map (add_multi add);
    1.33 +    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end);
    1.34  in
    1.35 -  val add_axioms           = add_singles Theory.add_axioms;
    1.36 -  val add_axioms_i         = add_singles Theory.add_axioms_i;
    1.37 -  val add_axiomss          = add_multis Theory.add_axioms;
    1.38 -  val add_axiomss_i        = add_multis Theory.add_axioms_i;
    1.39 -  val add_defs             = add_singles o Theory.add_defs false;
    1.40 -  val add_defs_i           = add_singles o Theory.add_defs_i false;
    1.41 -  val add_defs_unchecked   = add_singles o Theory.add_defs true;
    1.42 -  val add_defs_unchecked_i = add_singles o Theory.add_defs_i true;
    1.43 +  val add_axioms           = add_axm Theory.add_axioms;
    1.44 +  val add_axioms_i         = add_axm Theory.add_axioms_i;
    1.45 +  val add_defs             = add_axm o Theory.add_defs false;
    1.46 +  val add_defs_i           = add_axm o Theory.add_defs_i false;
    1.47 +  val add_defs_unchecked   = add_axm o Theory.add_defs true;
    1.48 +  val add_defs_unchecked_i = add_axm o Theory.add_defs_i true;
    1.49  end;
    1.50  
    1.51