diff -r 17414e2736f4 -r e03059ae2d82 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/type_infer.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -64,7 +64,7 @@
       else (inst, used);
     val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
     val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
-  in (map o map_types) (TermSubst.instantiateT inst) ts end;
+  in (map o map_types) (Term_Subst.instantiateT inst) ts end;