# HG changeset patch
# User wenzelm
# Date 1437940244 -7200
# Node ID 2f39d95ac55dcd4fdfa864828041122906e0eae9
# Parent  15f3da2636f5700041cbbf4143a65971697e0616
updated to infer_instantiate;

diff -r 15f3da2636f5 -r 2f39d95ac55d src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sun Jul 26 21:48:00 2015 +0200
+++ b/src/FOLP/simp.ML	Sun Jul 26 21:50:44 2015 +0200
@@ -543,14 +543,12 @@
 
 fun mk_cong ctxt (f,aTs,rT) (refl,eq) =
 let val k = length aTs;
-    fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
-        let val ca = Thm.cterm_of ctxt va
-            and cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T))
+    fun ri((subst,va as Var(a,Ta),vb as Var(b,Tb), Var (P, _)),i,si,T,yik) =
+        let val cx = Thm.cterm_of ctxt (eta_Var(("X"^si,0),T))
             val cb = Thm.cterm_of ctxt vb
-            and cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T))
-            val cP = Thm.cterm_of ctxt P
-            and cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs))
-        in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
+            val cy = Thm.cterm_of ctxt (eta_Var(("Y"^si,0),T))
+            val cp = Thm.cterm_of ctxt (Pinst(f,rT,eq,k,i,T,yik,aTs))
+        in infer_instantiate ctxt [(a,cx),(b,cy),(P,cp)] subst end;
     fun mk(c,T::Ts,i,yik) =
         let val si = radixstring(26,"a",i)
         in case find_subst ctxt T of