--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed Dec 08 22:17:52 2010 +0100
@@ -13,7 +13,7 @@
val fact_prefix : string
val conjecture_prefix : string
- val translate_fact :
+ val translate_atp_fact :
Proof.context -> (string * 'a) * thm
-> term * ((string * 'a) * translated_formula) option
val prepare_atp_problem :
@@ -247,7 +247,8 @@
|> map_filter (Option.map snd o make_fact ctxt false)
end
-fun translate_fact ctxt (ax as (_, th)) = (prop_of th, make_fact ctxt true ax)
+fun translate_atp_fact ctxt (ax as (_, th)) =
+ (prop_of th, make_fact ctxt true ax)
fun translate_formulas ctxt full_types hyp_ts concl_t facts =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100
@@ -31,7 +31,7 @@
datatype fact =
Untranslated of (string * locality) * thm |
- Translated of term * ((string * locality) * translated_formula) option
+ ATP_Translated of term * ((string * locality) * translated_formula) option
type prover_problem =
{state: Proof.state,
@@ -214,7 +214,7 @@
datatype fact =
Untranslated of (string * locality) * thm |
- Translated of term * ((string * locality) * translated_formula) option
+ ATP_Translated of term * ((string * locality) * translated_formula) option
type prover_problem =
{state: Proof.state,
@@ -268,9 +268,9 @@
(* generic TPTP-based ATPs *)
fun dest_Untranslated (Untranslated p) = p
- | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
-fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
- | translated_fact _ (Translated p) = p
+ | dest_Untranslated (ATP_Translated _) = raise Fail "dest_Untranslated"
+fun atp_translated_fact ctxt (Untranslated p) = translate_atp_fact ctxt p
+ | atp_translated_fact _ (ATP_Translated p) = p
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -289,7 +289,7 @@
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val facts =
- facts |> map (translated_fact ctxt)
+ facts |> map (atp_translated_fact ctxt)
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
val problem_prefix = Config.get ctxt problem_prefix
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100
@@ -29,7 +29,7 @@
val auto_max_relevant_divisor = 2
fun fact_name (Untranslated ((name, _), _)) = SOME name
- | fact_name (Translated (_, p)) = Option.map (fst o fst) p
+ | fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
relevance_thresholds, max_relevant, ...})
@@ -98,7 +98,7 @@
end
val run_atps =
run_provers "ATP" full_types atp_relevance_fudge
- (Translated o translate_fact ctxt) atps
+ (ATP_Translated o translate_atp_fact ctxt) atps
val run_smts =
run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
fun run_atps_and_smt_solvers () =