# HG changeset patch
# User blanchet
# Date 1343292483 -7200
# Node ID d443166f95202b12246a357e9d9550b1c117d9a8
# Parent  716ec3458b1dedc28bb34de0e036556faba429bb
repaired accessibility chains generated by MaSh exporter + tuned one function out

diff -r 716ec3458b1d -r d443166f9520 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -123,7 +123,8 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts =
-      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
+      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
+                                  Symtab.empty [] [] css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>
diff -r 716ec3458b1d -r d443166f9520 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -36,8 +36,9 @@
     val slack_max_facts = max_facts_slack * the max_facts
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts =
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
     val all_names = all_names (facts |> map snd)
     val mepo_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0
@@ -70,7 +71,7 @@
         val th =
           case find_first (fn (_, th) => nickname_of th = name) facts of
             SOME (_, th) => th
-          | NONE => error ("No fact called \"" ^ name ^ "\"")
+          | NONE => error ("No fact called \"" ^ name ^ "\".")
         val goal = goal_of_thm thy th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val isar_deps = isar_dependencies_of all_names th |> these
diff -r 716ec3458b1d -r d443166f9520 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -9,11 +9,11 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val generate_accessibility : theory -> bool -> string -> unit
+  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
   val generate_features :
     Proof.context -> string -> theory -> bool -> string -> unit
   val generate_isar_dependencies :
-    theory -> bool -> string -> unit
+    Proof.context -> theory -> bool -> string -> unit
   val generate_atp_dependencies :
     Proof.context -> params -> theory -> bool -> string -> unit
   val generate_commands : Proof.context -> params -> theory -> string -> unit
@@ -56,7 +56,7 @@
     SOME deps => deps
   | NONE => isar_dependencies_of all_names th |> these
 
-fun generate_accessibility thy include_thy file_name =
+fun generate_accessibility ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
@@ -65,24 +65,25 @@
         val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
         val _ = File.append path s
       in [fact] end
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val thy_map =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_facts ctxt false Symtab.empty [] [] css
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> thy_map_from_facts
     fun do_thy facts =
       let
         val thy = thy_of_fact thy (hd facts)
         val parents = parent_facts thy thy_map
-      in fold do_fact facts parents; () end
+      in fold_rev do_fact facts parents; () end
   in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
 
 fun generate_features ctxt prover thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val css_table = clasimpset_rule_table_of ctxt
+    val css = clasimpset_rule_table_of ctxt
     val facts =
-      all_facts_of (Proof_Context.init_global thy) css_table
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
       |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, stature), th) =
       let
@@ -93,12 +94,13 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_isar_dependencies thy include_thy file_name =
+fun generate_isar_dependencies ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val ths =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> map snd
     val all_names = all_names ths
@@ -116,8 +118,9 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val facts =
-      all_facts_of (Proof_Context.init_global thy) Termtab.empty
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = all_names ths
@@ -134,8 +137,9 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts =
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
@@ -164,8 +168,9 @@
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val prover = hd provers
-    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val facts = all_facts_of (Proof_Context.init_global thy) css_table
+    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts =
+      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
diff -r 716ec3458b1d -r d443166f9520 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
@@ -29,7 +29,9 @@
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
-  val all_facts_of : Proof.context -> status Termtab.table -> fact list
+  val all_facts :
+    Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
+    -> status Termtab.table -> fact list
   val nearly_all_facts :
     Proof.context -> bool -> fact_override -> unit Symtab.table
     -> status Termtab.table -> thm list -> term list -> term -> fact list
@@ -436,10 +438,6 @@
              |> op @
   end
 
-fun all_facts_of ctxt css =
-  all_facts ctxt false Symtab.empty [] [] css
-  |> rev (* partly restore the original order of facts, for MaSh *)
-
 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
                      concl_t =
   if only andalso null add then