src/FOLP/simp.ML
changeset 60790 2f39d95ac55d
parent 60789 15f3da2636f5
child 61268 abe08fb15a12
     1.1 --- a/src/FOLP/simp.ML	Sun Jul 26 21:48:00 2015 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sun Jul 26 21:50:44 2015 +0200
     1.3 @@ -543,14 +543,12 @@
     1.4  
     1.5  fun mk_cong ctxt (f,aTs,rT) (refl,eq) =
     1.6  let val k = length aTs;
     1.7 -    fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
     1.8 -        let val ca = Thm.cterm_of ctxt va
     1.9 -            and cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T))
    1.10 +    fun ri((subst,va as Var(a,Ta),vb as Var(b,Tb), Var (P, _)),i,si,T,yik) =
    1.11 +        let val cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T))
    1.12              val cb = Thm.cterm_of ctxt vb
    1.13 -            and cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T))
    1.14 -            val cP = Thm.cterm_of ctxt P
    1.15 -            and cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.16 -        in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
    1.17 +            val cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T))
    1.18 +            val cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs))
    1.19 +        in infer_instantiate ctxt [(a,cx),(b,cy),(P,cp)] subst end;
    1.20      fun mk(c,T::Ts,i,yik) =
    1.21          let val si = radixstring(26,"a",i)
    1.22          in case find_subst ctxt T of