--- a/src/HOL/TPTP/mash_export.ML Wed Dec 12 00:24:06 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Wed Dec 12 02:47:45 2012 +0100
@@ -28,11 +28,12 @@
structure MaSh_Export : MASH_EXPORT =
struct
+open Sledgehammer_Fact
open Sledgehammer_MePo
open Sledgehammer_MaSh
fun thy_map_from_facts ths =
- ths |> sort (thm_ord o swap o pairself snd)
+ ths |> rev
|> map (snd #> `(theory_of_thm #> Context.theory_name))
|> AList.coalesce (op =)
|> map (apsnd (map nickname_of))
@@ -45,6 +46,7 @@
fun all_facts ctxt =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
+ |> sort (thm_ord o pairself snd)
end
fun add_thy_parent_facts thy_map thy =
@@ -59,8 +61,6 @@
val thy_name_of_fact = hd o Long_Name.explode
fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact
-val all_names = map (rpair () o nickname_of) #> Symtab.make
-
fun generate_accessibility ctxt thys include_thys file_name =
let
val path = file_name |> Path.explode
@@ -110,18 +110,16 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts =
- all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
- val ths = facts |> map snd
- val all_names = all_names ths
- fun do_thm th =
+ all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
+ val all_names = build_all_names nickname_of facts
+ fun do_fact (_, th) =
let
val name = nickname_of th
val deps =
isar_or_prover_dependencies_of ctxt params_opt facts all_names th
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
- in List.app do_thm ths end
+ in List.app do_fact facts end
fun generate_isar_dependencies ctxt =
generate_isar_or_prover_dependencies ctxt NONE
@@ -134,10 +132,8 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = all_facts ctxt
- val (new_facts, old_facts) =
- facts |> List.partition (has_thys thys o snd)
- |>> sort (thm_ord o pairself snd)
- val all_names = all_names (map snd facts)
+ val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
+ val all_names = build_all_names nickname_of facts
fun do_fact ((_, stature), th) prevs =
let
val name = nickname_of th
@@ -171,9 +167,7 @@
val _ = File.write path ""
val prover = hd provers
val facts = all_facts ctxt
- val (new_facts, old_facts) =
- facts |> List.partition (has_thys thys o snd)
- |>> sort (thm_ord o pairself snd)
+ val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
fun do_fact (fact as (_, th)) old_facts =
let
val name = nickname_of th