compile

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue May 31 16:38:36 2011 +0200
@@ -335,7 +335,7 @@
     | NONE => get_prover (default_prover_name ()))
   end
 
-type locality = Sledgehammer_Filter.locality
+type locality = ATP_Translate.locality
 
 (* hack *)
 fun reconstructor_from_msg args msg =
@@ -361,7 +361,7 @@
     fun change_dir (SOME dir) =
         Config.put Sledgehammer_Provers.dest_dir dir
         #> Config.put SMT_Config.debug_files
-          (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"
+          (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
           ^ serial_string ())
       | change_dir NONE = I
     val st' =
@@ -391,14 +391,14 @@
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
     val relevance_override = {add = [], del = [], only = false}
-    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
-        preplay = K Sledgehammer_ATP_Reconstruct.Failed_to_Play,
+        preplay = K ATP_Reconstruct.Failed_to_Play,
         message = K ""}, ~1)
     val ({outcome, used_facts, run_time_in_msecs, preplay, message}
          : Sledgehammer_Provers.prover_result,
@@ -469,7 +469,7 @@
     case result of
       SH_OK (time_isa, time_prover, names) =>
         let
-          fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
+          fun get_thms (_, ATP_Translate.Chained) = NONE
             | get_thms (name, loc) =
               SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 31 16:38:36 2011 +0200
@@ -128,8 +128,7 @@
                (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
          val relevance_override = {add = [], del = [], only = false}
          val subgoal = 1
-         val (_, hyp_ts, concl_t) =
-           Sledgehammer_Util.strip_subgoal ctxt goal subgoal
+         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
          val facts =
            Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
                (the_default default_max_relevant max_relevant)

--- a/src/HOL/ex/sledgehammer_tactics.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Tue May 31 16:38:36 2011 +0200
@@ -32,7 +32,7 @@
     val relevance_fudge =
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     val relevance_override = {add = [], del = [], only = false}
-    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
+    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val facts =
       Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
           (the_default default_max_relevant max_relevant) (K true)

--- a/src/HOL/ex/tptp_export.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Tue May 31 16:38:36 2011 +0200
@@ -17,9 +17,9 @@
 structure TPTP_Export : TPTP_EXPORT =
 struct
 
-val ascii_of = Metis_Translate.ascii_of
+val ascii_of = ATP_Translate.ascii_of
 
-val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of
+val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
 
 fun facts_of thy =
   Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
@@ -60,9 +60,9 @@
         val s =
           "[" ^ Thm.legacy_get_kind thm ^ "] " ^
           (if member (op =) axioms name then "A" else "T") ^ " " ^
-          prefix Sledgehammer_ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
+          prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
           commas (theorems_mentioned_in_proof_term thm) ^ "; " ^
-          commas (map (prefix Metis_Translate.const_prefix o ascii_of)
+          commas (map (prefix ATP_Translate.const_prefix o ascii_of)
                       (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
       in File.append path s end
     val thms = facts_of thy |> map (snd o snd)
@@ -91,21 +91,21 @@
   let
     val format = ATP_Problem.FOF
     val type_sys =
-      Sledgehammer_ATP_Translate.Preds
-          (Sledgehammer_ATP_Translate.Polymorphic,
-           if full_types then Sledgehammer_ATP_Translate.All_Types
-           else Sledgehammer_ATP_Translate.Const_Arg_Types,
-           Sledgehammer_ATP_Translate.Heavy)
+      ATP_Translate.Preds
+          (ATP_Translate.Polymorphic,
+           if full_types then ATP_Translate.All_Types
+           else ATP_Translate.Const_Arg_Types,
+           ATP_Translate.Heavy)
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts0 = facts_of thy
     val facts =
       facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
-                    Sledgehammer_ATP_Translate.translate_atp_fact ctxt format
+                    ATP_Translate.translate_atp_fact ctxt format
                     type_sys true ((Thm.get_name_hint th, loc), th)))
     val explicit_apply = NONE
     val (atp_problem, _, _, _, _, _, _) =
-      Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format
+      ATP_Translate.prepare_atp_problem ctxt format
           ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []
           @{prop False} facts
     val infers =