src/FOLP/simp.ML
changeset 14772 c52060b69a8c
parent 14643 130076a81b84
child 15531 08c8dad8e399
     1.1 --- a/src/FOLP/simp.ML	Fri May 21 21:17:37 2004 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri May 21 21:18:14 2004 +0200
     1.3 @@ -549,7 +549,7 @@
     1.4          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
     1.5              val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
     1.6              val eqT::_ = binder_types cT
     1.7 -        in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
     1.8 +        in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
     1.9             else find thms
    1.10          end
    1.11        | find [] = None
    1.12 @@ -581,7 +581,7 @@
    1.13      val tsig = Sign.tsig_of sg;
    1.14      fun find_refl(r::rs) =
    1.15          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
    1.16 -        in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
    1.17 +        in if Type.typ_instance tsig (rT, hd(binder_types eqT))
    1.18             then Some(r,(eq,body_type eqT)) else find_refl rs
    1.19          end
    1.20        | find_refl([]) = None;