--- a/src/Pure/drule.ML Sat Feb 10 09:26:26 2007 +0100
+++ b/src/Pure/drule.ML Sat Feb 10 16:43:23 2007 +0100
@@ -910,7 +910,7 @@
fun instT(ct,cu) =
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)
+ fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy (Envir.norm_type tye T))
in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end
handle TERM _ =>
raise THM("cterm_instantiate: incompatible theories",0,[th])