src/Pure/Isar/locale.ML

           if is_local then I
           else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>
             TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
     val rename =
           if is_local then I
-          else Term.map_term_types renameT;
+          else Term.map_types renameT;
 
     val tinst = Symtab.make (map
                 (fn ((x, 0), T) => (x, T |> renameT)
                   | ((_, n), _) => sys_error "Internal error var in prep_registration") vinst);
     val inst = Symtab.make (given_ps ~~ map rename vs);