--- a/src/Provers/hypsubst.ML Thu Jun 09 22:25:25 2011 +0200
+++ b/src/Provers/hypsubst.ML Thu Jun 09 23:12:02 2011 +0200
@@ -163,7 +163,7 @@
| t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
val thy = Thm.theory_of_thm rl';
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
- in compose_tac (true, Drule.instantiate (instT,
+ in compose_tac (true, Drule.instantiate_normalize (instT,
map (pairself (cterm_of thy))
[(Var (ixn, Ts ---> U --> body_type T), u),
(Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),