diff -r b1965c8992c8 -r a44b0fdaa6c2 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 13:26:39 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 13:52:23 2011 +0200
@@ -125,7 +125,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val T = domain_type (fastype_of t);
     val T' = fastype_of u;
-    val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
+    val subst = Sign.typ_match thy (T, T') Vartab.empty
       handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
   in
     map_types (Envir.norm_type subst) t $ u