src/HOL/Tools/refute.ML
changeset 15574 b1d1b5bfc464
parent 15571 c166086feace
child 15611 c01f11cd08f9
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -788,14 +788,14 @@
     1.4  								else
     1.5  									acc)
     1.6  							(* collect argument types *)
     1.7 -							val acc_args = Library.foldr collect_types (Ts, acc')
     1.8 +							val acc_args = foldr collect_types acc' Ts
     1.9  							(* collect constructor types *)
    1.10 -							val acc_constrs = Library.foldr collect_types (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
    1.11 +							val acc_constrs = foldr collect_types acc_args (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs))
    1.12  						in
    1.13  							acc_constrs
    1.14  						end
    1.15  					| NONE =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
    1.16 -						T ins (Library.foldr collect_types (Ts, acc)))
    1.17 +						T ins (foldr collect_types acc Ts))
    1.18  				| TFree _                => T ins acc
    1.19  				| TVar _                 => T ins acc)
    1.20  	in
    1.21 @@ -1297,8 +1297,8 @@
    1.22  	let
    1.23  		val Ts = binder_types (fastype_of t)
    1.24  	in
    1.25 -		Library.foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
    1.26 -			(Library.take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
    1.27 +		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
    1.28 +			(list_comb (t, map Bound (i-1 downto 0))) (Library.take (i, Ts))
    1.29  	end;
    1.30  
    1.31  (* ------------------------------------------------------------------------- *)
    1.32 @@ -2234,7 +2234,7 @@
    1.33  					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
    1.34  					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
    1.35  				in
    1.36 -					SOME (Library.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
    1.37 +					SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set pairs)
    1.38  				end
    1.39  			| Type ("prop", [])      =>
    1.40  				(case index_from_interpretation intr of