src/HOL/Tools/refute.ML
changeset 16331 386ce655d694
parent 16200 447c06881fbb
child 16366 6ff17d08c3d5
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Jun 09 12:03:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jun 09 12:03:18 2005 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4  	let
     1.5  		val _ = immediate_output "Adding axioms..."
     1.6  		(* (string * Term.term) list *)
     1.7 -		val axioms = List.concat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
     1.8 +		val axioms = Theory.all_axioms_of thy;
     1.9  		(* string list *)
    1.10  		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
    1.11  			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)