diff -r a63605582573 -r 016f3be5a5ec src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Apr 21 19:13:03 2005 +0200
@@ -260,13 +260,14 @@
 fun typ_subst env = apsnd (Term.typ_subst_TVars env);
 fun subst env = apsnd (Term.subst_TVars env);
 
-fun instantiate sign envT env =
+fun instantiate sign envT env thm =
   let
-    fun prepT (a, T) = (a, Thm.ctyp_of sign T);
+    val (_, sorts) = Drule.types_sorts thm;
+    fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T);
     fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
   in
     Drule.instantiate (map prepT (distinct envT),
-      map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env))
+      map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
   end;
 
 in
@@ -309,8 +310,8 @@
     (* internal term instantiations *)
 
     val types' = #1 (Drule.types_sorts thm');
-    val unifier = Vartab.dest (#1
-      (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts)));
+    val unifier = map (apsnd snd) (Vartab.dest (#1
+      (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))));
 
     val type_insts'' = map (typ_subst unifier) type_insts';
     val internal_insts'' = map (subst unifier) internal_insts;