diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -247,7 +247,7 @@
     val U = Term.fastype_of u;
     val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
   in
-    Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
+    Sign.typ_unify thy (T, U) (unifier, maxidx')
       handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
   end;