src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^
       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "")
     end
 
 val e_config : atp_config =
-  {exec = (["E_HOME"], ["eprover"]),
+  {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn problem =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        ["--auto-schedule --tstp-in --tstp-out --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^
         e_term_order_info_arguments gen_weights gen_prec ord_info ^