src/Pure/Isar/rule_insts.ML

     Sign.typ_unify thy (T, U) (unifier, maxidx')
       handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
   end;
 
 fun instantiate inst =
-  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
   Envir.beta_norm;
 
 fun make_instT f v =
   let
     val T = TVar v;

         if Sign.of_sort thy (T, S) then ((xi, S), T)
         else error_var "Incompatible sort for typ instantiation of " xi
       end;
 
     val type_insts1 = map readT type_insts;
-    val instT1 = Term.instantiateT type_insts1;
+    val instT1 = TermSubst.instantiateT type_insts1;
     val vars1 = map (apsnd instT1) vars;
 
 
     (* internal term instantiations *)