# HG changeset patch
# User blanchet
# Date 1277116423 -7200
# Node ID d5a85d35ef62b247f8255be5a2f9c25bab304f58
# Parent  f6b1ee5b420bdc7c749a838f1b08d964e33b8614
thread "full_types"

diff -r f6b1ee5b420b -r d5a85d35ef62 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 21 12:31:41 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 21 12:33:43 2010 +0200
@@ -336,8 +336,9 @@
 
 (* start prover thread *)
 
-fun start_prover_thread (params as {timeout, ...}) birth_time death_time i n
-                        relevance_override minimize_command proof_state name =
+fun start_prover_thread (params as {full_types, timeout, ...}) birth_time
+                        death_time i n relevance_override minimize_command
+                        proof_state name =
   let
     val prover = get_prover (Proof.theory_of proof_state) name
     val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -353,7 +354,7 @@
            filtered_clauses = NONE}
         val message =
           #message (prover params (minimize_command name) timeout problem)
-          handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n []
+          handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n []
                | ERROR message => "Error: " ^ message ^ "\n"
         val _ = unregister params message (Thread.self ());
       in () end)
diff -r f6b1ee5b420b -r d5a85d35ef62 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 21 12:31:41 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 21 12:33:43 2010 +0200
@@ -222,9 +222,9 @@
       case outcome of
         NONE =>
         proof_text isar_proof
-            (pool, debug, full_types, isar_shrink_factor, ctxt,
-             conjecture_shape)
-            (minimize_command, proof, internal_thm_names, th, subgoal)
+            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+            (full_types, minimize_command, proof, internal_thm_names, th,
+             subgoal)
       | SOME failure => (string_for_failure failure ^ "\n", [])
   in
     {outcome = outcome, message = message, pool = pool,
@@ -249,7 +249,7 @@
       (relevant_facts full_types respect_no_atp relevance_threshold
                       relevance_convergence defs_relevant max_axiom_clauses
                       (the_default prefers_theory_relevant theory_relevant))
-      (prepare_clauses false)
+      (prepare_clauses false full_types)
       (write_tptp_file (debug andalso overlord)) home_var
       executable (arguments timeout) proof_delims known_failures name params
       minimize_command
@@ -323,7 +323,7 @@
       (relevant_facts full_types respect_no_atp relevance_threshold
                       relevance_convergence defs_relevant max_axiom_clauses
                       (the_default prefers_theory_relevant theory_relevant))
-      (prepare_clauses true) write_dfg_file home_var executable
+      (prepare_clauses true full_types) write_dfg_file home_var executable
       (arguments timeout) proof_delims known_failures name params
       minimize_command