# 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