# HG changeset patch
# User wenzelm
# Date 1269215478 -3600
# Node ID 28e73b3e7b6cc70675b4cd57467be4ee2aa93d82
# Parent  f81557a124d56a257280cab60f169415e95609f1
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

diff -r f81557a124d5 -r 28e73b3e7b6c src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Mar 22 00:48:56 2010 +0100
+++ b/src/Pure/more_thm.ML	Mon Mar 22 00:51:18 2010 +0100
@@ -337,8 +337,8 @@
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
-    val thy' = thy
-      |> Theory.add_axioms_i [(b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'))];
+    val thy' =
+      Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b');
     val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
   in (thm, thy') end;
diff -r f81557a124d5 -r 28e73b3e7b6c src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Mar 22 00:48:56 2010 +0100
+++ b/src/Pure/theory.ML	Mon Mar 22 00:51:18 2010 +0100
@@ -28,8 +28,7 @@
   val at_end: (theory -> theory option) -> theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
-  val add_axioms_i: (binding * term) list -> theory -> theory
-  val add_axioms: (binding * string) list -> theory -> theory
+  val add_axiom: binding * term -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
   val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
   val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
@@ -171,23 +170,14 @@
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
 
-(* add_axioms(_i) *)
+(* add_axiom *)
 
-local
-
-fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
+fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd Logic.varify_global o prep_axm thy) raw_axms;
-    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
+    val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
+    val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
   in axioms' end);
 
-in
-
-val add_axioms_i = gen_add_axioms cert_axm;
-val add_axioms = gen_add_axioms read_axm;
-
-end;
-
 
 
 (** add constant definitions **)
@@ -269,7 +259,7 @@
   let val axms = map (prep_axm thy) raw_axms in
     thy
     |> map_defs (fold (check_def thy unchecked overloaded) axms)
-    |> add_axioms_i axms
+    |> fold add_axiom axms
   end;
 
 in