src/HOL/Tools/refute.ML
changeset 20854 f9cf9e62d11c
parent 20548 8ef25fe585a8
child 21056 2cfe839e8d58
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -785,7 +785,7 @@
     1.4  									())
     1.5  							(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
     1.6  							val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
     1.7 -									T ins acc
     1.8 +									insert (op =) T acc
     1.9  								else
    1.10  									acc)
    1.11  							(* collect argument types *)
    1.12 @@ -796,9 +796,9 @@
    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 (foldr collect_types acc Ts))
    1.17 -				| TFree _                => T ins acc
    1.18 -				| TVar _                 => T ins acc)
    1.19 +						insert (op =) T (foldr collect_types acc Ts))
    1.20 +				| TFree _                => insert (op =) T acc
    1.21 +				| TVar _                 => insert (op =) T acc)
    1.22  	in
    1.23  		it_term_types collect_types (t, [])
    1.24  	end;