Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Tools/refute.ML
changeset 14810 4b4b97d29370
parent 14807 e8ccb13d7774
child 14818 ad83019a66a4 
     1.1 --- a/src/HOL/Tools/refute.ML	Wed May 26 18:23:46 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed May 26 18:52:18 2004 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4  									Library.exists (fn c =>
     1.5  										(case c of
     1.6  										  Const (cname, ctype) =>
     1.7 -											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T, ctype)
     1.8 +											cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
     1.9  										| _ =>
    1.10  											raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
    1.11  										constrs
    1.12 @@ -1566,7 +1566,7 @@
    1.13  											())
    1.14  									(* split the constructors into those occuring before/after 'Const (s, T)' *)
    1.15  									val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
    1.16 -										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy), T,
    1.17 +										not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
    1.18  											map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
    1.19  								in
    1.20  									case constrs2 of
isabelle