src/HOL/Tools/ATP/atp_systems.ML

      |> map (fn (s, w) => "," ^ s ^ ":" ^
                           scaled_e_selection_weight ctxt heuristic w)
      |> implode) ^
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
-    \FIFOWeight(PreferProcessed))'"
+    \FIFOWeight(PreferProcessed))' "
   else
-    "-xAuto"
+    "-xAuto "
 
 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 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 "")
+      (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 = fn full_proofs => (["E_HOME"],
      if full_proofs orelse not (is_e_at_least_1_8 ()) then ["eproof_ram", "eproof"]
      else ["eprover"]),
    arguments = fn ctxt => fn full_proofs => fn heuristic => fn timeout => fn file_name =>
      fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        (if is_e_at_least_1_8 () then "--auto-schedule " else "") ^
        "--tstp-in --tstp-out --silent " ^
-       e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
-       e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
+       e_selection_weight_arguments ctxt heuristic sel_weights ^
+       e_term_order_info_arguments gen_weights gen_prec ord_info ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
        (if full_proofs orelse not (is_e_at_least_1_8 ()) then
           " --output-level=5 --pcl-shell-level=" ^ (if full_proofs then "0" else "2")
         else