1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 09 23:23:12 2012 +0200
     1.3 @@ -28,8 +28,6 @@
     1.4  open ATP_Problem_Generate
     1.5  open ATP_Systems
     1.6  
     1.7 -val thy_prefix = "$"
     1.8 -
     1.9  fun stringN_of_int 0 _ = ""
    1.10    | stringN_of_int k n =
    1.11      stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
    1.12 @@ -40,19 +38,19 @@
    1.13      String.str c
    1.14    else
    1.15      (* fixed width, in case more digits follow *)
    1.16 -    "_" ^ stringN_of_int 3 (Char.ord c)
    1.17 +    "~" ^ stringN_of_int 3 (Char.ord c)
    1.18  val escape_meta = String.translate escape_meta_char
    1.19  
    1.20  val fact_name_of = escape_meta
    1.21 -val thy_name_of = prefix thy_prefix o escape_meta
    1.22 +val thy_name_of = escape_meta
    1.23  
    1.24  fun facts_of thy =
    1.25    let val ctxt = Proof_Context.init_global thy in
    1.26 -    Sledgehammer_Filter.all_facts ctxt false
    1.27 -        Symtab.empty true [] []
    1.28 +    Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
    1.29          (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
    1.30      |> filter (curry (op =) @{typ bool} o fastype_of
    1.31                 o Object_Logic.atomize_term thy o prop_of o snd)
    1.32 +    |> rev
    1.33    end
    1.34  
    1.35  (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    1.36 @@ -104,30 +102,31 @@
    1.37    let
    1.38      val path = file_name |> Path.explode
    1.39      val _ = File.write path ""
    1.40 -    fun do_thm parents th seen =
    1.41 +    val thy_name_of_thm = theory_of_thm #> Context.theory_name
    1.42 +    fun do_thm th prevs =
    1.43        let
    1.44 -        val s = th ^ ": " ^ space_implode " " (parents @ seen) ^ "\n"
    1.45 +        val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
    1.46          val _ = File.append path s
    1.47 -      in seen @ [th] end
    1.48 -    fun do_thy (name, ths) =
    1.49 +      in [th] end
    1.50 +    val thy_ths =
    1.51 +      facts_of thy
    1.52 +      |> map (snd #> `thy_name_of_thm)
    1.53 +      |> AList.group (op =)
    1.54 +      |> sort (theory_ord o pairself (theory_of_thm o hd o snd))
    1.55 +      |> map (apsnd (sort (theory_ord o pairself theory_of_thm)))
    1.56 +    fun do_thy ths =
    1.57        let
    1.58 -        val ths = sort (theory_ord o pairself theory_of_thm) ths
    1.59          val thy = theory_of_thm (hd ths)
    1.60          val parents =
    1.61 -          if Context.theory_name thy = Context.theory_name @{theory HOL} then []
    1.62 -          else map (thy_name_of o Context.theory_name) (Theory.parents_of thy)
    1.63 -        val ths = map (fact_name_of o Thm.get_name_hint) ths
    1.64 -        val s =
    1.65 -          thy_name_of name ^ ": " ^ space_implode " " (parents @ ths) ^ " \n"
    1.66 -        val _ = File.append path s
    1.67 -        val _ = fold (do_thm parents) ths []
    1.68 +          Theory.parents_of thy
    1.69 +          |> map (thy_name_of o Context.theory_name)
    1.70 +          |> map_filter (AList.lookup (op =) thy_ths)
    1.71 +          |> map List.last
    1.72 +          |> map (fact_name_of o Thm.get_name_hint)
    1.73 +        val ths = ths |> map (fact_name_of o Thm.get_name_hint)
    1.74 +        val _ = fold do_thm ths parents
    1.75        in () end
    1.76 -    val thy_name_of_thm = theory_of_thm #> Context.theory_name
    1.77 -    val thy_ths =
    1.78 -      facts_of thy |> map (snd #> `thy_name_of_thm)
    1.79 -                   |> AList.group (op =)
    1.80 -                   |> sort (theory_ord o pairself (theory_of_thm o hd o snd))
    1.81 -    val _ = List.app do_thy thy_ths
    1.82 +    val _ = List.app (do_thy o snd) thy_ths
    1.83    in () end
    1.84  
    1.85  (* TODO: Add types, subterms, intro/dest/elim/simp status *)