# HG changeset patch
# User paulson
# Date 1171122203 -3600
# Node ID bb31094b487925addc5dde41a077f53d284e57f6
# Parent  a532c39c891722952058f819798e61733ca4da15
Completing the bug fix from the previous update: the result of unifying type
variables must be normalized WRT itself; otherwise instantiation is wrong

diff -r a532c39c8917 -r bb31094b4879 src/Pure/drule.ML
--- 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])