removed "sorts" option, continued

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 28 13:00:30 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 28 13:32:45 2010 +0200
@@ -25,7 +25,6 @@
      follow_defs: bool,
      isar_proof: bool,
      shrink_factor: int,
-     sorts: bool,
      timeout: Time.time,
      minimize_timeout: Time.time}
   type problem =
@@ -85,7 +84,6 @@
    follow_defs: bool,
    isar_proof: bool,
    shrink_factor: int,
-   sorts: bool,
    timeout: Time.time,
    minimize_timeout: Time.time}
 

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Apr 28 13:00:30 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Apr 28 13:32:45 2010 +0200
@@ -110,8 +110,8 @@
 
 fun generic_prover overlord get_facts prepare write_file home executable args
         proof_delims known_failures name
-        ({debug, full_types, explicit_apply, isar_proof, shrink_factor, sorts,
-         ...} : params) minimize_command
+        ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...}
+         : params) minimize_command
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -213,7 +213,7 @@
       case outcome of
         NONE =>
         proof_text isar_proof
-                   (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)
+                   (pool, debug, shrink_factor, ctxt, conjecture_shape)
                    (minimize_command, proof, internal_thm_names, th, subgoal)
       | SOME failure => (string_for_failure failure ^ "\n", [])
   in