# HG changeset patch
# User wenzelm
# Date 1118311398 -7200
# Node ID 386ce655d6949137a33ef21f1998ae1cb4fe6588
# Parent  934219e919e40ae1a8d21798c5b6297967bc8392
Theory.all_axioms_of;

diff -r 934219e919e4 -r 386ce655d694 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Jun 09 12:03:17 2005 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Jun 09 12:03:18 2005 +0200
@@ -419,7 +419,7 @@
 	let
 		val _ = immediate_output "Adding axioms..."
 		(* (string * Term.term) list *)
-		val axioms = List.concat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
+		val axioms = Theory.all_axioms_of thy;
 		(* string list *)
 		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
 			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
diff -r 934219e919e4 -r 386ce655d694 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Jun 09 12:03:17 2005 +0200
+++ b/src/Pure/codegen.ML	Thu Jun 09 12:03:18 2005 +0200
@@ -383,8 +383,7 @@
 
 fun get_defn thy s T =
   let
-    val axms = List.concat (map (Symtab.dest o #axioms o Theory.rep_theory)
-      (thy :: Theory.ancestors_of thy));
+    val axms = Theory.all_axioms_of thy;
     fun prep_def def = (case preprocess thy [def] of
       [def'] => prop_of def' | _ => error "get_defn: bad preprocessor");
     fun dest t =