--- a/src/Provers/hypsubst.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Provers/hypsubst.ML Sun Jul 05 15:02:30 2015 +0200
@@ -186,10 +186,10 @@
val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
in
compose_tac ctxt (true, Drule.instantiate_normalize (instT,
- map (apply2 (Thm.cterm_of ctxt))
- [(Var (ixn, Ts ---> U --> body_type T), u),
- (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
- (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
+ map (apsnd (Thm.cterm_of ctxt))
+ [((ixn, Ts ---> U --> body_type T), u),
+ ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
+ ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
Thm.nprems_of rl) i
end
| NONE => no_tac);