--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:14:47 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:15:07 2010 +0200
@@ -19,7 +19,6 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
-open Clausifier
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
@@ -134,7 +133,7 @@
filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
- (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
+ c = (if pos then "c_False" else "c_True")
| is_false_literal _ = false
fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
(pol andalso c = "c_True") orelse
@@ -185,7 +184,7 @@
fun cnf_helper_thms thy raw =
map (`Thm.get_name_hint)
- #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true)
+ #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
val optional_helpers =
[(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
@@ -256,7 +255,7 @@
(* get clauses and prepare them for writing *)
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt;
- val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
+ val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
case filtered_clauses of
@@ -265,7 +264,7 @@
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
- |> cnf_rules_pairs thy true
+ |> Clausifier.cnf_rules_pairs thy true
val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses