--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200
@@ -309,8 +309,7 @@
val params = Sledgehammer_Isar.default_params thy []
val problem =
{subgoal = 1, goal = (ctxt', (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axiom_clauses = NONE, filtered_clauses = NONE}
+ relevance_override = {add = [], del = [], only = false}, axioms = NONE}
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200
@@ -30,7 +30,7 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option}
+ axioms: (string * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
@@ -98,7 +98,7 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option}
+ axioms: (string * thm) list option}
type prover_result =
{outcome: failure option,
@@ -355,16 +355,14 @@
map (s_not o HOLogic.dest_Trueprop) hyp_ts @
[HOLogic.dest_Trueprop concl_t]
|> make_conjecture_clauses ctxt
- val (clnames, axiom_clauses) =
- ListPair.unzip (map (make_axiom_clause ctxt) axcls)
+ val (clnames, axioms) = ListPair.unzip (map (make_axiom_clause ctxt) axcls)
val helper_clauses =
- get_helper_clauses ctxt is_FO full_types conjectures axiom_clauses
+ get_helper_clauses ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
(Vector.fromList clnames,
- (conjectures, axiom_clauses, helper_clauses, class_rel_clauses,
- arity_clauses))
+ (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses))
end
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
@@ -587,10 +585,10 @@
(const_table_for_problem explicit_apply problem) problem
fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
- file (conjectures, axiom_clauses, helper_clauses,
+ file (conjectures, axioms, helper_clauses,
class_rel_clauses, arity_clauses) =
let
- val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
+ val axiom_lines = map (problem_line_for_axiom full_types) axioms
val class_rel_lines =
map problem_line_for_class_rel_clause class_rel_clauses
val arity_lines = map problem_line_for_arity_clause arity_clauses
@@ -675,15 +673,15 @@
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
isar_shrink_factor, ...} : params)
minimize_command timeout
- ({subgoal, goal, relevance_override, axiom_clauses} : problem) =
+ ({subgoal, goal, relevance_override, axioms} : problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt
(* ### FIXME: (1) preprocessing for "if" etc. *)
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
- val the_axiom_clauses =
- case axiom_clauses of
+ val the_axioms =
+ case axioms of
SOME axioms => axioms
| NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant
@@ -691,7 +689,7 @@
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
val (internal_thm_names, clauses) =
- prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
+ prepare_clauses ctxt full_types hyp_ts concl_t the_axioms
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -824,7 +822,7 @@
let
val problem =
{subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE}
+ relevance_override = relevance_override, axioms = NONE}
in
prover params (minimize_command name) timeout problem |> #message
handle ERROR message => "Error: " ^ message ^ "\n"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:39:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:42:09 2010 +0200
@@ -38,22 +38,22 @@
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
name_thms_pairs =
let
- val num_theorems = length name_thms_pairs
+ val num_axioms = length name_thms_pairs
val _ =
- priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^
- (if num_theorems > 0 then
+ priority ("Testing " ^ string_of_int num_axioms ^
+ " theorem" ^ plural_s num_axioms ^
+ (if num_axioms > 0 then
": " ^ space_implode " "
(name_thms_pairs
|> map fst |> sort_distinct string_ord)
else
"") ^ "...")
- val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+ val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME name_thm_pairs}
+ axioms = SOME axioms}
in
prover params (K "") timeout problem
|> tap (fn result : prover_result =>