src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

     {blocking: bool,
      debug: bool,
      verbose: bool,
      overlord: bool,
      provers: string list,
+     type_sys: string,
      full_types: bool,
-     type_sys: string,
      explicit_apply: bool,
      relevance_thresholds: real * real,
      max_relevant: int option,
      isar_proof: bool,
      isar_shrink_factor: int,

   {blocking: bool,
    debug: bool,
    verbose: bool,
    overlord: bool,
    provers: string list,
+   type_sys: string,
    full_types: bool,
-   type_sys: string,
    explicit_apply: bool,
    relevance_thresholds: real * real,
    max_relevant: int option,
    isar_proof: bool,
    isar_shrink_factor: int,

 val important_message_keep_factor = 0.1
 
 fun run_atp auto atp_name
         ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
          known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
-        ({debug, verbose, overlord, full_types, type_sys, explicit_apply,
+        ({debug, verbose, overlord, type_sys, full_types, explicit_apply,
           isar_proof, isar_shrink_factor, timeout, ...} : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val type_sys =

     val (message, used_facts) =
       case outcome of
         NONE =>
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-            (proof_banner auto, full_types, minimize_command, tstplike_proof,
+            (proof_banner auto, type_sys, minimize_command, tstplike_proof,
              fact_names, goal, subgoal)
         |>> (fn message =>
                 message ^
                 (if verbose then
                    "\nATP real CPU time: " ^