| changeset 60642 | 48dd1cefb4ae |
| parent 59632 | 5980e75a204e |
| child 66551 | 4df6b0ae900d |
--- a/src/HOL/Tools/SMT/smt_util.ML Fri Jul 03 16:19:45 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_util.ML Sun Jul 05 15:02:30 2015 +0200 @@ -171,7 +171,7 @@ val destT1 = hd o Thm.dest_ctyp val destT2 = hd o tl o Thm.dest_ctyp -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct)