src/HOL/Tools/refute.ML
changeset 21078 101aefd61aac
parent 21056 2cfe839e8d58
child 21098 d0d8a48ae4e6
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:25 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Oct 20 17:07:26 2006 +0200
     1.3 @@ -421,8 +421,8 @@
     1.4  		(* (string * Term.term) list *)
     1.5  		val axioms = Theory.all_axioms_of thy;
     1.6  		(* string list *)
     1.7 -		val rec_names = Symtab.fold (fn (_, info) => fn acc =>
     1.8 -			#rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
     1.9 +		val rec_names = Symtab.fold (append o #rec_names o snd)
    1.10 +          (DatatypePackage.get_datatypes thy) [];
    1.11  		(* string list *)
    1.12  		val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
    1.13  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.14 @@ -677,7 +677,7 @@
    1.15  					fun is_IDT_recursor () =
    1.16  						(* I'm not quite sure if checking the name 's' is sufficient, *)
    1.17  						(* or if we should also check the type 'T'                    *)
    1.18 -						s mem rec_names
    1.19 +						member (op =) rec_names s
    1.20  				in
    1.21  					if is_const_of_class () then
    1.22  						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)