1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 21 12:31:41 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 21 12:33:43 2010 +0200
     1.3 @@ -336,8 +336,9 @@
     1.4  
     1.5  (* start prover thread *)
     1.6  
     1.7 -fun start_prover_thread (params as {timeout, ...}) birth_time death_time i n
     1.8 -                        relevance_override minimize_command proof_state name =
     1.9 +fun start_prover_thread (params as {full_types, timeout, ...}) birth_time
    1.10 +                        death_time i n relevance_override minimize_command
    1.11 +                        proof_state name =
    1.12    let
    1.13      val prover = get_prover (Proof.theory_of proof_state) name
    1.14      val {context = ctxt, facts, goal} = Proof.goal proof_state;
    1.15 @@ -353,7 +354,7 @@
    1.16             filtered_clauses = NONE}
    1.17          val message =
    1.18            #message (prover params (minimize_command name) timeout problem)
    1.19 -          handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n []
    1.20 +          handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n []
    1.21                 | ERROR message => "Error: " ^ message ^ "\n"
    1.22          val _ = unregister params message (Thread.self ());
    1.23        in () end)

     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 21 12:31:41 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 21 12:33:43 2010 +0200
     2.3 @@ -222,9 +222,9 @@
     2.4        case outcome of
     2.5          NONE =>
     2.6          proof_text isar_proof
     2.7 -            (pool, debug, full_types, isar_shrink_factor, ctxt,
     2.8 -             conjecture_shape)
     2.9 -            (minimize_command, proof, internal_thm_names, th, subgoal)
    2.10 +            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    2.11 +            (full_types, minimize_command, proof, internal_thm_names, th,
    2.12 +             subgoal)
    2.13        | SOME failure => (string_for_failure failure ^ "\n", [])
    2.14    in
    2.15      {outcome = outcome, message = message, pool = pool,
    2.16 @@ -249,7 +249,7 @@
    2.17        (relevant_facts full_types respect_no_atp relevance_threshold
    2.18                        relevance_convergence defs_relevant max_axiom_clauses
    2.19                        (the_default prefers_theory_relevant theory_relevant))
    2.20 -      (prepare_clauses false)
    2.21 +      (prepare_clauses false full_types)
    2.22        (write_tptp_file (debug andalso overlord)) home_var
    2.23        executable (arguments timeout) proof_delims known_failures name params
    2.24        minimize_command
    2.25 @@ -323,7 +323,7 @@
    2.26        (relevant_facts full_types respect_no_atp relevance_threshold
    2.27                        relevance_convergence defs_relevant max_axiom_clauses
    2.28                        (the_default prefers_theory_relevant theory_relevant))
    2.29 -      (prepare_clauses true) write_dfg_file home_var executable
    2.30 +      (prepare_clauses true full_types) write_dfg_file home_var executable
    2.31        (arguments timeout) proof_delims known_failures name params
    2.32        minimize_command
    2.33