src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

   (member (op =) [@{const_name HOL.eq}] s orelse
    case type_sys of
      Many_Typed => false
    | Tags full_types => full_types orelse s = explicit_app_base
    | Args _ => s = explicit_app_base
-   | Mangled _ => s = explicit_app_base
+   | Mangled _ => false
    | No_Types => true)
 
 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
 
 fun type_arg_policy type_sys s =

        (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
        strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
      | _ => ([], f ty))
   | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
 
-fun problem_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
+fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) =
   let
     val thy = Proof_Context.theory_of ctxt
     val arity = min_arity_of thy type_sys sym_tab s
   in
     if type_sys = Many_Typed then
       let
         val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
         val (s, s') = (s, s') |> mangled_const_name ty_args
       in
-        Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
+        Decl (sym_decl_prefix ^ ascii_of s, (s, s'),
+              arg_tys,
               if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
       end
     else
       let
         val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty
         val bounds =
           map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
           ~~ map SOME arg_tys
         val bound_tms =
           map (fn (name, ty) => CombConst (name, the ty, [])) bounds
+        val freshener =
+          case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
       in
-        Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
+        Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
                  CombConst ((s, s'), ty, ty_args)
                  |> fold (curry (CombApp o swap)) bound_tms
                  |> type_pred_combatom type_sys res_ty
                  |> mk_aquant AForall bounds
                  |> formula_for_combformula ctxt type_sys,
                  NONE, NONE)
       end
   end
 fun problem_lines_for_const ctxt type_sys sym_tab (s, xs) =
-  map (problem_line_for_const_entry ctxt type_sys sym_tab s) xs
+  map2 (problem_line_for_typed_const ctxt type_sys sym_tab s)
+       (0 upto length xs - 1) xs
 
 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
     union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   | add_tff_types_in_formula (AConn (_, phis)) =
     fold add_tff_types_in_formula phis