diff -r eaa5d6987ba2 -r 4b4b97d29370 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed May 26 18:23:46 2004 +0200
+++ b/src/HOL/Tools/refute.ML	Wed May 26 18:52:18 2004 +0200
@@ -600,7 +600,7 @@
 									Library.exists (fn c =>
 										(case c of
 										  Const (cname, ctype) =>
-											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T, ctype)
+											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
 										| _ =>
 											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
 										constrs
@@ -1566,7 +1566,7 @@
 											())
 									(* split the constructors into those occuring before/after 'Const (s, T)' *)
 									val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
-										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T,
+										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
 											map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
 								in
 									case constrs2 of