# HG changeset patch
# User blanchet
# Date 1272454365 -7200
# Node ID 2b2a2c55d78732d6f82e6a3bb92a6f126e39c538
# Parent  32c92af68ec9a77e36eea7661102efc0c0b9a52d
removed "sorts" option, continued

diff -r 32c92af68ec9 -r 2b2a2c55d787 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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}
 
diff -r 32c92af68ec9 -r 2b2a2c55d787 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- 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