diff -r 8c5d44c7e8af -r 30bedf58b177 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -20,8 +20,8 @@
      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,
@@ -204,8 +204,8 @@
    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,
@@ -271,7 +271,7 @@
 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
@@ -398,7 +398,7 @@
         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 ^