1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -8,11 +8,7 @@
     1.4  signature ATP_THEORY_EXPORT =
     1.5  sig
     1.6    type atp_format = ATP_Problem.atp_format
     1.7 -  type stature = Sledgehammer_Filter.stature
     1.8  
     1.9 -  val theorems_mentioned_in_proof_term :
    1.10 -    string list option -> thm -> string list
    1.11 -  val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list
    1.12    val generate_atp_inference_file_for_theory :
    1.13      Proof.context -> theory -> atp_format -> string -> string -> unit
    1.14  end;
    1.15 @@ -27,45 +23,6 @@
    1.16  
    1.17  val fact_name_of = prefix fact_prefix o ascii_of
    1.18  
    1.19 -(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    1.20 -   fixes that seem to be missing over there; or maybe the two code portions are
    1.21 -   not doing the same? *)
    1.22 -fun fold_body_thms thm_name f =
    1.23 -  let
    1.24 -    fun app n (PBody {thms, ...}) =
    1.25 -      thms |> fold (fn (_, (name, prop, body)) => fn x =>
    1.26 -        let
    1.27 -          val body' = Future.join body
    1.28 -          val n' =
    1.29 -            n + (if name = "" orelse
    1.30 -                    (* uncommon case where the proved theorem occurs twice
    1.31 -                       (e.g., "Transitive_Closure.trancl_into_trancl") *)
    1.32 -                    (n = 1 andalso name = thm_name) then
    1.33 -                   0
    1.34 -                 else
    1.35 -                   1)
    1.36 -          val x' = x |> n' <= 1 ? app n' body'
    1.37 -        in (x' |> n = 1 ? f (name, prop, body')) end)
    1.38 -  in fold (app 0) end
    1.39 -
    1.40 -fun theorems_mentioned_in_proof_term all_names th =
    1.41 -  let
    1.42 -    val is_name_ok =
    1.43 -      case all_names of
    1.44 -        SOME names => member (op =) names
    1.45 -      | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
    1.46 -    fun collect (s, _, _) = is_name_ok s ? insert (op =) s
    1.47 -    val names =
    1.48 -      [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
    1.49 -  in names end
    1.50 -
    1.51 -fun all_facts_of_theory thy =
    1.52 -  let val ctxt = Proof_Context.init_global thy in
    1.53 -    Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
    1.54 -        (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
    1.55 -    |> rev (* try to restore the original order of facts, for MaSh *)
    1.56 -  end
    1.57 -
    1.58  fun inference_term [] = NONE
    1.59    | inference_term ss =
    1.60      ATerm (("inference", []),
    1.61 @@ -153,7 +110,7 @@
    1.62      val mono = not (is_type_enc_polymorphic type_enc)
    1.63      val path = file_name |> Path.explode
    1.64      val _ = File.write path ""
    1.65 -    val facts = all_facts_of_theory thy
    1.66 +    val facts = Sledgehammer_Fact.all_facts_of thy
    1.67      val atp_problem =
    1.68        facts
    1.69        |> map (fn ((_, loc), th) =>
    1.70 @@ -170,7 +127,7 @@
    1.71      val infers =
    1.72        facts |> map (fn (_, th) =>
    1.73                         (fact_name_of (Thm.get_name_hint th),
    1.74 -                        th |> theorems_mentioned_in_proof_term (SOME all_names)
    1.75 +                        th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
    1.76                             |> map fact_name_of))
    1.77      val all_atp_problem_names =
    1.78        atp_problem |> maps (map ident_of_problem_line o snd)