changeset 31977 | e03059ae2d82 |
parent 30146 | a77fc0209723 |
child 32002 | 1a35de4112bb |
--- 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;