1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 08 22:17:52 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 08 22:17:52 2010 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5    val fact_prefix : string
     1.6    val conjecture_prefix : string
     1.7 -  val translate_fact :
     1.8 +  val translate_atp_fact :
     1.9      Proof.context -> (string * 'a) * thm
    1.10      -> term * ((string * 'a) * translated_formula) option
    1.11    val prepare_atp_problem :
    1.12 @@ -247,7 +247,8 @@
    1.13      |> map_filter (Option.map snd o make_fact ctxt false)
    1.14    end
    1.15  
    1.16 -fun translate_fact ctxt (ax as (_, th)) = (prop_of th, make_fact ctxt true ax)
    1.17 +fun translate_atp_fact ctxt (ax as (_, th)) =
    1.18 +  (prop_of th, make_fact ctxt true ax)
    1.19  
    1.20  fun translate_formulas ctxt full_types hyp_ts concl_t facts =
    1.21    let

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:52 2010 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4  
     2.5    datatype fact =
     2.6      Untranslated of (string * locality) * thm |
     2.7 -    Translated of term * ((string * locality) * translated_formula) option
     2.8 +    ATP_Translated of term * ((string * locality) * translated_formula) option
     2.9  
    2.10    type prover_problem =
    2.11      {state: Proof.state,
    2.12 @@ -214,7 +214,7 @@
    2.13  
    2.14  datatype fact =
    2.15    Untranslated of (string * locality) * thm |
    2.16 -  Translated of term * ((string * locality) * translated_formula) option
    2.17 +  ATP_Translated of term * ((string * locality) * translated_formula) option
    2.18  
    2.19  type prover_problem =
    2.20    {state: Proof.state,
    2.21 @@ -268,9 +268,9 @@
    2.22  (* generic TPTP-based ATPs *)
    2.23  
    2.24  fun dest_Untranslated (Untranslated p) = p
    2.25 -  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
    2.26 -fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
    2.27 -  | translated_fact _ (Translated p) = p
    2.28 +  | dest_Untranslated (ATP_Translated _) = raise Fail "dest_Untranslated"
    2.29 +fun atp_translated_fact ctxt (Untranslated p) = translate_atp_fact ctxt p
    2.30 +  | atp_translated_fact _ (ATP_Translated p) = p
    2.31  
    2.32  fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
    2.33    | int_opt_add _ _ = NONE
    2.34 @@ -289,7 +289,7 @@
    2.35      val ctxt = Proof.context_of state
    2.36      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    2.37      val facts =
    2.38 -      facts |> map (translated_fact ctxt)
    2.39 +      facts |> map (atp_translated_fact ctxt)
    2.40      val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.41                     else Config.get ctxt dest_dir
    2.42      val problem_prefix = Config.get ctxt problem_prefix

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 08 22:17:52 2010 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  val auto_max_relevant_divisor = 2
     3.5  
     3.6  fun fact_name (Untranslated ((name, _), _)) = SOME name
     3.7 -  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
     3.8 +  | fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p
     3.9  
    3.10  fun run_sledgehammer (params as {blocking, debug, provers, full_types,
    3.11                                   relevance_thresholds, max_relevant, ...})
    3.12 @@ -98,7 +98,7 @@
    3.13            end
    3.14        val run_atps =
    3.15          run_provers "ATP" full_types atp_relevance_fudge
    3.16 -                    (Translated o translate_fact ctxt) atps
    3.17 +                    (ATP_Translated o translate_atp_fact ctxt) atps
    3.18        val run_smts =
    3.19          run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
    3.20        fun run_atps_and_smt_solvers () =