# HG changeset patch
# User paulson
# Date 1170954853 -3600
# Node ID 9985a79735c7cc470a7ef087e9ee905fbb8ac61a
# Parent  85b065601f4558ac252203b8099373aafac98a86
cterm_instantiate was calling a type instantiation function that works only for matching,
not unification as here.

diff -r 85b065601f45 -r 9985a79735c7 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Feb 08 17:22:22 2007 +0100
+++ b/src/Pure/drule.ML	Thu Feb 08 18:14:13 2007 +0100
@@ -908,7 +908,7 @@
 fun cterm_instantiate ctpairs0 th =
   let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
       fun instT(ct,cu) =
-        let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
+        let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
         in (inst ct, inst cu) end
       fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end