# HG changeset patch
# User blanchet
# Date 1291843072 -3600
# Node ID 54eb8e7c7f9bd874aa2b370a2bfbece236fa7fcb
# Parent  d7b5fd465198fba26b72899cca7c1eb3bc15350c
clarified terminology

diff -r d7b5fd465198 -r 54eb8e7c7f9b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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
diff -r d7b5fd465198 -r 54eb8e7c7f9b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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
diff -r d7b5fd465198 -r 54eb8e7c7f9b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- 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 () =