clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;

--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Oct 22 20:55:13 2019 +0200
@@ -322,15 +322,6 @@
 \<close>
 
 ML \<open>
-val axms_of_thy =
-  `Theory.axioms_of
-  #> apsnd cterm_of
-  #> swap
-  #> apsnd (map snd)
-  #> uncurry map
-\<close>
-
-ML \<open>
 (*Show the skeleton-level inference which is done by each element of just_the_tacs. This is useful when debugging using the technique shown next*)
 if test_all @{context} orelse prob_names = [] then ()
 else

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 22 20:55:13 2019 +0200
@@ -1338,8 +1338,7 @@
           |> maps snd |> map_filter #def
           |> Ord_List.make fast_string_ord
   in
-    Theory.nodes_of thy
-    |> maps Thm.axioms_of
+    Thm.all_axioms_of thy
     |> map (apsnd (subst_atomic subst o Thm.prop_of))
     |> sort (fast_string_ord o apply2 fst)
     |> Ord_List.inter (fast_string_ord o apsnd fst) def_names

--- a/src/Pure/Thy/export_theory.ML	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Oct 22 20:55:13 2019 +0200
@@ -242,8 +242,8 @@
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =
-      export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
-        Theory.axiom_space (Theory.axioms_of thy);
+      export_entities "axioms" (K (SOME o encode_axiom Name.context))
+        Theory.axiom_space (Theory.all_axioms_of thy);
 
 
     (* theorems and proof terms *)

--- a/src/Pure/theory.ML	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/Pure/theory.ML	Tue Oct 22 20:55:13 2019 +0200
@@ -18,7 +18,6 @@
   val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
-  val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
@@ -88,18 +87,17 @@
 structure Thy = Theory_Data'
 (
   type T = thy;
-  val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
-  val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
+  val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], []));
 
-  fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
-    make_thy (Position.none, 0, empty_axioms, defs, wrappers);
+  fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) =
+    make_thy (Position.none, 0, axioms, defs, wrappers);
 
   fun merge old_thys (thy1, thy2) =
     let
-      val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
-      val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
+      val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+      val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
-      val axioms' = empty_axioms;
+      val axioms' = Name_Space.merge_tables (axioms1, axioms2);
       val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
@@ -163,8 +161,7 @@
 val axiom_table = #axioms o rep_theory;
 val axiom_space = Name_Space.space_of_table o axiom_table;
 
-val axioms_of = Name_Space.dest_table o axiom_table;
-fun all_axioms_of thy = maps axioms_of (nodes_of thy);
+val all_axioms_of = Name_Space.dest_table o axiom_table;
 
 val defs_of = #defs o rep_theory;
 

--- a/src/Pure/thm.ML	Tue Oct 22 20:08:25 2019 +0200
+++ b/src/Pure/thm.ML	Tue Oct 22 20:55:13 2019 +0200
@@ -113,7 +113,7 @@
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
-  val axioms_of: theory -> (string * thm) list
+  val all_axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T
   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   val norm_proof: thm -> thm
@@ -804,30 +804,23 @@
 
 (** Axioms **)
 
-fun axiom thy0 name =
-  let
-    fun get_ax thy =
-      Name_Space.lookup (Theory.axiom_table thy) name
-      |> Option.map (fn prop =>
-           let
-             val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
-             val cert = Context.Certificate thy;
-             val maxidx = maxidx_of_term prop;
-             val shyps = Sorts.insert_term prop [];
-           in
-             Thm (der,
-               {cert = cert, tags = [], maxidx = maxidx,
-                 constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop})
-           end);
-  in
-    (case get_first get_ax (Theory.nodes_of thy0) of
-      SOME thm => thm
-    | NONE => raise THEORY ("No axiom " ^ quote name, [thy0]))
-  end;
+fun axiom thy name =
+  (case Name_Space.lookup (Theory.axiom_table thy) name of
+    SOME prop =>
+      let
+        val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
+        val cert = Context.Certificate thy;
+        val maxidx = maxidx_of_term prop;
+        val shyps = Sorts.insert_term prop [];
+      in
+        Thm (der,
+          {cert = cert, tags = [], maxidx = maxidx,
+            constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop})
+      end
+  | NONE => raise THEORY ("No axiom " ^ quote name, [thy]));
 
-(*return additional axioms of this theory node*)
-fun axioms_of thy =
-  map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy);
+fun all_axioms_of thy =
+  map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy);
 
 
 (* tags *)