src/Pure/type_infer.ML
changeset 31977 e03059ae2d82
parent 30146 a77fc0209723
child 32002 1a35de4112bb
     1.1 --- a/src/Pure/type_infer.ML	Thu Jul 09 22:36:11 2009 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Jul 09 22:48:12 2009 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4        else (inst, used);
     1.5      val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
     1.6      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
     1.7 -  in (map o map_types) (TermSubst.instantiateT inst) ts end;
     1.8 +  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
     1.9  
    1.10  
    1.11