1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -123,7 +123,8 @@
     1.4      val path = file_name |> Path.explode
     1.5      val _ = File.write path ""
     1.6      val facts =
     1.7 -      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     1.8 +      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false
     1.9 +                                  Symtab.empty [] [] css_table
    1.10      val atp_problem =
    1.11        facts
    1.12        |> map (fn ((_, loc), th) =>

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Thu Jul 26 10:48:03 2012 +0200
     2.3 @@ -36,8 +36,9 @@
     2.4      val slack_max_facts = max_facts_slack * the max_facts
     2.5      val path = file_name |> Path.explode
     2.6      val lines = path |> File.read_lines
     2.7 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     2.8 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
     2.9 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.10 +    val facts =
    2.11 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    2.12      val all_names = all_names (facts |> map snd)
    2.13      val mepo_ok = Unsynchronized.ref 0
    2.14      val mash_ok = Unsynchronized.ref 0
    2.15 @@ -70,7 +71,7 @@
    2.16          val th =
    2.17            case find_first (fn (_, th) => nickname_of th = name) facts of
    2.18              SOME (_, th) => th
    2.19 -          | NONE => error ("No fact called \"" ^ name ^ "\"")
    2.20 +          | NONE => error ("No fact called \"" ^ name ^ "\".")
    2.21          val goal = goal_of_thm thy th
    2.22          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.23          val isar_deps = isar_dependencies_of all_names th |> these

     3.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
     3.3 @@ -9,11 +9,11 @@
     3.4  sig
     3.5    type params = Sledgehammer_Provers.params
     3.6  
     3.7 -  val generate_accessibility : theory -> bool -> string -> unit
     3.8 +  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
     3.9    val generate_features :
    3.10      Proof.context -> string -> theory -> bool -> string -> unit
    3.11    val generate_isar_dependencies :
    3.12 -    theory -> bool -> string -> unit
    3.13 +    Proof.context -> theory -> bool -> string -> unit
    3.14    val generate_atp_dependencies :
    3.15      Proof.context -> params -> theory -> bool -> string -> unit
    3.16    val generate_commands : Proof.context -> params -> theory -> string -> unit
    3.17 @@ -56,7 +56,7 @@
    3.18      SOME deps => deps
    3.19    | NONE => isar_dependencies_of all_names th |> these
    3.20  
    3.21 -fun generate_accessibility thy include_thy file_name =
    3.22 +fun generate_accessibility ctxt thy include_thy file_name =
    3.23    let
    3.24      val path = file_name |> Path.explode
    3.25      val _ = File.write path ""
    3.26 @@ -65,24 +65,25 @@
    3.27          val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
    3.28          val _ = File.append path s
    3.29        in [fact] end
    3.30 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.31      val thy_map =
    3.32 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    3.33 +      all_facts ctxt false Symtab.empty [] [] css
    3.34        |> not include_thy ? filter_out (has_thy thy o snd)
    3.35        |> thy_map_from_facts
    3.36      fun do_thy facts =
    3.37        let
    3.38          val thy = thy_of_fact thy (hd facts)
    3.39          val parents = parent_facts thy thy_map
    3.40 -      in fold do_fact facts parents; () end
    3.41 +      in fold_rev do_fact facts parents; () end
    3.42    in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
    3.43  
    3.44  fun generate_features ctxt prover thy include_thy file_name =
    3.45    let
    3.46      val path = file_name |> Path.explode
    3.47      val _ = File.write path ""
    3.48 -    val css_table = clasimpset_rule_table_of ctxt
    3.49 +    val css = clasimpset_rule_table_of ctxt
    3.50      val facts =
    3.51 -      all_facts_of (Proof_Context.init_global thy) css_table
    3.52 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    3.53        |> not include_thy ? filter_out (has_thy thy o snd)
    3.54      fun do_fact ((_, stature), th) =
    3.55        let
    3.56 @@ -93,12 +94,13 @@
    3.57        in File.append path s end
    3.58    in List.app do_fact facts end
    3.59  
    3.60 -fun generate_isar_dependencies thy include_thy file_name =
    3.61 +fun generate_isar_dependencies ctxt thy include_thy file_name =
    3.62    let
    3.63      val path = file_name |> Path.explode
    3.64      val _ = File.write path ""
    3.65 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.66      val ths =
    3.67 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    3.68 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    3.69        |> not include_thy ? filter_out (has_thy thy o snd)
    3.70        |> map snd
    3.71      val all_names = all_names ths
    3.72 @@ -116,8 +118,9 @@
    3.73      val path = file_name |> Path.explode
    3.74      val _ = File.write path ""
    3.75      val prover = hd provers
    3.76 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.77      val facts =
    3.78 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    3.79 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    3.80        |> not include_thy ? filter_out (has_thy thy o snd)
    3.81      val ths = facts |> map snd
    3.82      val all_names = all_names ths
    3.83 @@ -134,8 +137,9 @@
    3.84      val path = file_name |> Path.explode
    3.85      val _ = File.write path ""
    3.86      val prover = hd provers
    3.87 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.88 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
    3.89 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    3.90 +    val facts =
    3.91 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    3.92      val (new_facts, old_facts) =
    3.93        facts |> List.partition (has_thy thy o snd)
    3.94              |>> sort (thm_ord o pairself snd)
    3.95 @@ -164,8 +168,9 @@
    3.96      val path = file_name |> Path.explode
    3.97      val _ = File.write path ""
    3.98      val prover = hd provers
    3.99 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   3.100 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
   3.101 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   3.102 +    val facts =
   3.103 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
   3.104      val (new_facts, old_facts) =
   3.105        facts |> List.partition (has_thy thy o snd)
   3.106              |>> sort (thm_ord o pairself snd)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 26 10:48:03 2012 +0200
     4.3 @@ -29,7 +29,9 @@
     4.4      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     4.5      -> (((unit -> string) * 'a) * thm) list
     4.6    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
     4.7 -  val all_facts_of : Proof.context -> status Termtab.table -> fact list
     4.8 +  val all_facts :
     4.9 +    Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
    4.10 +    -> status Termtab.table -> fact list
    4.11    val nearly_all_facts :
    4.12      Proof.context -> bool -> fact_override -> unit Symtab.table
    4.13      -> status Termtab.table -> thm list -> term list -> term -> fact list
    4.14 @@ -436,10 +438,6 @@
    4.15               |> op @
    4.16    end
    4.17  
    4.18 -fun all_facts_of ctxt css =
    4.19 -  all_facts ctxt false Symtab.empty [] [] css
    4.20 -  |> rev (* partly restore the original order of facts, for MaSh *)
    4.21 -
    4.22  fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
    4.23                       concl_t =
    4.24    if only andalso null add then