--- 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)
--- 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 =