Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 37347 635425a442e8
parent 37346 cdba266f0383
child 37413 e856582fe9c4 
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:08:35 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:39:23 2010 +0200
@@ -239,14 +239,14 @@
 fun generic_tptp_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
-        (params as {debug, overlord, respect_no_atp, relevance_threshold,
-                    relevance_convergence, theory_relevant, defs_relevant,
-                    isar_proof, ...})
+        (params as {debug, overlord, full_types, respect_no_atp,
+                    relevance_threshold, relevance_convergence, theory_relevant,
+                    defs_relevant, isar_proof, ...})
         minimize_command timeout =
   generic_prover overlord
-      (get_relevant_facts respect_no_atp relevance_threshold
-                          relevance_convergence defs_relevant max_axiom_clauses
-                          (the_default prefers_theory_relevant theory_relevant))
+      (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)
       (write_tptp_file (debug andalso overlord)) home_var
       executable (arguments timeout) proof_delims known_failures name params
@@ -314,13 +314,13 @@
 fun generic_dfg_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
-        (params as {overlord, respect_no_atp, relevance_threshold,
+        (params as {overlord, full_types, respect_no_atp, relevance_threshold,
                     relevance_convergence, theory_relevant, defs_relevant, ...})
         minimize_command timeout =
   generic_prover overlord
-      (get_relevant_facts respect_no_atp relevance_threshold
-                          relevance_convergence defs_relevant max_axiom_clauses
-                          (the_default prefers_theory_relevant theory_relevant))
+      (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
       (arguments timeout) proof_delims known_failures name params
       minimize_command
isabelle