Completing the bug fix from the previous update: the result of unifying type
variables must be normalized WRT itself; otherwise instantiation is wrong

--- 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])