src/Pure/Isar/element.ML

   if Symtab.is_empty env then I
   else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x));
 
 fun instT_term env =
   if Symtab.is_empty env then I
-  else Term.map_term_types (instT_type env);
+  else Term.map_types (instT_type env);
 
 fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
   (fn T as TFree (a, _) =>
     let val T' = the_default T (Symtab.lookup env a)
     in if T = T' then I else insert (op =) (a, T') end