# HG changeset patch
# User wenzelm
# Date 786987729 -3600
# Node ID df8f91c0e57c5fd5bda927c148d18719b3a9f6fd
# Parent  7b60621e2bada94d17358b341a237e697690fc89
improved axioms_of: returns thms as the manual says;

diff -r 7b60621e2bad -r df8f91c0e57c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Dec 09 13:39:52 1994 +0100
+++ b/src/Pure/drule.ML	Fri Dec 09 16:42:09 1994 +0100
@@ -110,7 +110,8 @@
 fun ancestry_of thy =
   thy :: flat (map ancestry_of (parents_of thy));
 
-val all_axioms_of = flat o map axioms_of o ancestry_of;
+val all_axioms_of = 
+  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
 
 
 (* clash_types, clash_consts *)
diff -r 7b60621e2bad -r df8f91c0e57c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 09 13:39:52 1994 +0100
+++ b/src/Pure/thm.ML	Fri Dec 09 16:42:09 1994 +0100
@@ -64,7 +64,7 @@
   val add_simps		: meta_simpset * thm list -> meta_simpset
   val assume		: cterm -> thm
   val assumption	: int -> thm -> thm Sequence.seq
-  val axioms_of		: theory -> (string * term) list
+  val axioms_of		: theory -> (string * thm) list
   val beta_conversion	: cterm -> thm
   val bicompose		: bool -> bool * thm * int -> int -> thm -> 
                           thm Sequence.seq
@@ -265,9 +265,6 @@
 (*stamps associated with a theory*)
 val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
 
-(*return additional axioms of this theory node*)
-val axioms_of = Symtab.dest o #new_axioms o rep_theory;
-
 (*return the immediate ancestors*)
 val parents_of = #parents o rep_theory;
 
@@ -291,6 +288,11 @@
       => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory])
   end;
 
+(*return additional axioms of this theory node*)
+fun axioms_of thy =
+  map (fn (s, _) => (s, get_axiom thy s))
+    (Symtab.dest (#new_axioms (rep_theory thy)));
+
 
 (* the Pure theory *)