# 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