src/HOL/Tools/ATP/atp_translate.ML

       else fold (fact_lift add_formula_var_types) (conjs @ facts) []
     fun add_undefined_const T =
       let
         val (s, s') =
           `make_fixed_const @{const_name undefined}
-          |> mangled_const_name format type_enc [T]
+          |> (case type_arg_policy type_enc @{const_name undefined} of
+                Mangled_Type_Args _ => mangled_const_name format type_enc [T]
+              | _ => I)
       in
         Symtab.map_default (s, [])
                            (insert_type ctxt #3 (s', [T], T, false, 0, false))
       end
   in