src/HOL/Tools/refute.ML
changeset 21056 2cfe839e8d58
parent 20854 f9cf9e62d11c
child 21078 101aefd61aac
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 19 12:08:27 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Oct 20 10:44:33 2006 +0200
     1.3 @@ -421,10 +421,10 @@
     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.foldl (fn (acc, (_, info)) =>
     1.8 -			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
     1.9 +		val rec_names = Symtab.fold (fn (_, info) => fn acc =>
    1.10 +			#rec_names info @ acc) (DatatypePackage.get_datatypes thy) []
    1.11  		(* string list *)
    1.12 -		val const_of_class_names = map Logic.const_of_class (Sign.classes (sign_of thy))
    1.13 +		val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
    1.14  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.15  		(* 't' has a (possibly) more general type, the schematic type          *)
    1.16  		(* variables in 't' are instantiated to match the type 'T' (may raise  *)
    1.17 @@ -1891,12 +1891,12 @@
    1.18  		                      (* terms has had a chance to look at 't'               *)
    1.19  		  (Const (s, T), params) =>
    1.20  			(* iterate over all datatypes in 'thy' *)
    1.21 -			Symtab.foldl (fn (result, (_, info)) =>
    1.22 +			Symtab.fold (fn (_, info) => fn result =>
    1.23  				case result of
    1.24  				  SOME _ =>
    1.25  					result  (* just keep 'result' *)
    1.26  				| NONE =>
    1.27 -					if s mem (#rec_names info) then
    1.28 +					if member (op =) (#rec_names info) s then
    1.29  						(* we do have a recursion operator of the datatype given by 'info', *)
    1.30  						(* or of a mutually recursive datatype                              *)
    1.31  						let
    1.32 @@ -2069,7 +2069,7 @@
    1.33  						end
    1.34  					else
    1.35  						NONE  (* not a recursion operator of this datatype *)
    1.36 -				) (NONE, DatatypePackage.get_datatypes thy)
    1.37 +				) (DatatypePackage.get_datatypes thy) NONE
    1.38  		| _ =>  (* head of term is not a constant *)
    1.39  			NONE;
    1.40