src/HOL/Tools/refute.ML
changeset 16935 4d7f19d340e8
parent 16424 18a07ad8fea8
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Jul 28 15:19:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jul 28 15:19:51 2005 +0200
     1.3 @@ -434,7 +434,7 @@
     1.4  		let
     1.5  			fun find_typeSubs (Const (s', T')) =
     1.6  				(if s=s' then
     1.7 -					SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) handle Type.TYPE_MATCH => NONE
     1.8 +					SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE
     1.9  				else
    1.10  					NONE)
    1.11  			  | find_typeSubs (Free _)           = NONE
    1.12 @@ -543,7 +543,7 @@
    1.13  							  SOME T' =>
    1.14  								let
    1.15  									val T''      = (domain_type o domain_type) T'
    1.16 -									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
    1.17 +									val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
    1.18  								in
    1.19  									SOME (axname, monomorphic_term typeSubs ax)
    1.20  								end
    1.21 @@ -642,7 +642,7 @@
    1.22  						in
    1.23  							if s=s' then
    1.24  								let
    1.25 -									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
    1.26 +									val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
    1.27  								in
    1.28  									SOME (axname, monomorphic_term typeSubs ax)
    1.29  								end
    1.30 @@ -668,7 +668,7 @@
    1.31  								Library.exists (fn c =>
    1.32  									(case c of
    1.33  									  Const (cname, ctype) =>
    1.34 -										cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
    1.35 +										cname = s andalso Sign.typ_instance thy (T, ctype)
    1.36  									| _ =>
    1.37  										raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
    1.38  									constrs
    1.39 @@ -1738,7 +1738,7 @@
    1.40  									())
    1.41  							(* split the constructors into those occuring before/after 'Const (s, T)' *)
    1.42  							val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
    1.43 -								not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
    1.44 +								not (cname = s andalso Sign.typ_instance thy (T,
    1.45  									map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
    1.46  						in
    1.47  							case constrs2 of