src/HOL/Tools/refute.ML
changeset 19642 ea7162f84677
parent 19346 c4c003abd830
child 20073 da82b545d2de
     1.1 --- a/src/HOL/Tools/refute.ML	Tue May 16 13:01:23 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue May 16 13:01:24 2006 +0200
     1.3 @@ -507,7 +507,7 @@
     1.4  					| _               => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
     1.5  				(* obtain all superclasses of classes in 'sort' *)
     1.6  				(* string list *)
     1.7 -				val superclasses = Graph.all_succs ((#2 o #classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
     1.8 +				val superclasses = distinct (op =) (sort @ maps (Sign.super_classes thy) sort)
     1.9  			in
    1.10  				Library.foldl collect_class_axioms (axs, superclasses)
    1.11  			end