# HG changeset patch
# User blanchet
# Date 1277743602 -7200
# Node ID 3e78dbf7a38259025d010292abdbcac66e040e5b
# Parent  537beae999d738d897218012be84ff19c9c2a27b
adapt call

diff -r 537beae999d7 -r 3e78dbf7a382 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 28 18:15:40 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Jun 28 18:46:42 2010 +0200
@@ -8,7 +8,6 @@
 
 signature ATP_MANAGER =
 sig
-  type cnf_thm = Clausifier.cnf_thm
   type name_pool = Metis_Clauses.name_pool
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
@@ -31,8 +30,8 @@
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
      relevance_override: relevance_override,
-     axiom_clauses: cnf_thm list option,
-     filtered_clauses: cnf_thm list option}
+     axiom_clauses: ((string * int) * thm) list option,
+     filtered_clauses: ((string * int) * thm) list option}
   datatype failure =
     Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
     MalformedInput | MalformedOutput | UnknownError
@@ -46,7 +45,7 @@
      proof: string,
      internal_thm_names: string Vector.vector,
      conjecture_shape: int list list,
-     filtered_clauses: cnf_thm list}
+     filtered_clauses: ((string * int) * thm) list}
   type prover =
     params -> minimize_command -> Time.time -> problem -> prover_result
 
@@ -98,8 +97,8 @@
   {subgoal: int,
    goal: Proof.context * (thm list * thm),
    relevance_override: relevance_override,
-   axiom_clauses: cnf_thm list option,
-   filtered_clauses: cnf_thm list option}
+   axiom_clauses: ((string * int) * thm) list option,
+   filtered_clauses: ((string * int) * thm) list option}
 
 datatype failure =
   Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
@@ -115,7 +114,7 @@
    proof: string,
    internal_thm_names: string Vector.vector,
    conjecture_shape: int list list,
-   filtered_clauses: cnf_thm list}
+   filtered_clauses: ((string * int) * thm) list}
 
 type prover =
   params -> minimize_command -> Time.time -> problem -> prover_result
diff -r 537beae999d7 -r 3e78dbf7a382 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 28 18:15:40 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jun 28 18:46:42 2010 +0200
@@ -139,12 +139,13 @@
     val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
     val goal_cls = List.concat goal_clss
     val the_filtered_clauses =
-      (case filtered_clauses of
-        NONE => relevant_facts full_types relevance_threshold
+      case filtered_clauses of
+        SOME fcls => fcls
+      | NONE => relevant_facts full_types relevance_threshold
                     relevance_convergence defs_relevant max_axiom_clauses
                     (the_default prefers_theory_relevant theory_relevant)
                     relevance_override goal goal_cls
-      | SOME fcls => fcls);
+                |> cnf_rules_pairs thy
     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