src/HOL/Tools/ATP/atp_problem_generate.ML

         (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
         (if needs_sound then typed_helper_suffix else untyped_helper_suffix)
       fun specialize_helper t T =
         if unmangled_s = app_op_name then
           let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in
-            monomorphic_term tyenv t
+            Envir.subst_term_types tyenv t
           end
         else
           specialize_type thy (invert_const unmangled_s, T) t
       fun dub_and_inst needs_sound ((status, t), j) =
         (if should_specialize_helper type_enc t then