src/HOL/Tools/ATP/atp_systems.ML

 val e_ord_weights =
   map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
 fun e_ord_precedence [_] = ""
   | e_ord_precedence info = info |> map fst |> space_implode "<"
 
-fun e_term_order_info_arguments _ false false _ = ""
-  | e_term_order_info_arguments ctxt gen_weights gen_prec ord_info =
+fun e_term_order_info_arguments false false _ = ""
+  | e_term_order_info_arguments gen_weights gen_prec ord_info =
     let val ord_info = ord_info () in
       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
        else "") ^
       (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
        else "")

    arguments =
      fn ctxt => fn _ => fn heuristic => fn timeout =>
         fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
         "--tstp-in --tstp-out --output-level=5 --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
-        e_term_order_info_arguments ctxt gen_weights gen_prec ord_info ^ " " ^
+        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
         "--term-ordering=" ^ (if is_lpo then "LPO4" else "Auto") ^ " " ^
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      known_szs_status_failures @