1.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -9,11 +9,11 @@
     1.4  sig
     1.5    type params = Sledgehammer_Provers.params
     1.6  
     1.7 -  val generate_accessibility : theory -> bool -> string -> unit
     1.8 +  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
     1.9    val generate_features :
    1.10      Proof.context -> string -> theory -> bool -> string -> unit
    1.11    val generate_isar_dependencies :
    1.12 -    theory -> bool -> string -> unit
    1.13 +    Proof.context -> theory -> bool -> string -> unit
    1.14    val generate_atp_dependencies :
    1.15      Proof.context -> params -> theory -> bool -> string -> unit
    1.16    val generate_commands : Proof.context -> params -> theory -> string -> unit
    1.17 @@ -56,7 +56,7 @@
    1.18      SOME deps => deps
    1.19    | NONE => isar_dependencies_of all_names th |> these
    1.20  
    1.21 -fun generate_accessibility thy include_thy file_name =
    1.22 +fun generate_accessibility ctxt thy include_thy file_name =
    1.23    let
    1.24      val path = file_name |> Path.explode
    1.25      val _ = File.write path ""
    1.26 @@ -65,24 +65,25 @@
    1.27          val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
    1.28          val _ = File.append path s
    1.29        in [fact] end
    1.30 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.31      val thy_map =
    1.32 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    1.33 +      all_facts ctxt false Symtab.empty [] [] css
    1.34        |> not include_thy ? filter_out (has_thy thy o snd)
    1.35        |> thy_map_from_facts
    1.36      fun do_thy facts =
    1.37        let
    1.38          val thy = thy_of_fact thy (hd facts)
    1.39          val parents = parent_facts thy thy_map
    1.40 -      in fold do_fact facts parents; () end
    1.41 +      in fold_rev do_fact facts parents; () end
    1.42    in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end
    1.43  
    1.44  fun generate_features ctxt prover thy include_thy file_name =
    1.45    let
    1.46      val path = file_name |> Path.explode
    1.47      val _ = File.write path ""
    1.48 -    val css_table = clasimpset_rule_table_of ctxt
    1.49 +    val css = clasimpset_rule_table_of ctxt
    1.50      val facts =
    1.51 -      all_facts_of (Proof_Context.init_global thy) css_table
    1.52 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.53        |> not include_thy ? filter_out (has_thy thy o snd)
    1.54      fun do_fact ((_, stature), th) =
    1.55        let
    1.56 @@ -93,12 +94,13 @@
    1.57        in File.append path s end
    1.58    in List.app do_fact facts end
    1.59  
    1.60 -fun generate_isar_dependencies thy include_thy file_name =
    1.61 +fun generate_isar_dependencies ctxt thy include_thy file_name =
    1.62    let
    1.63      val path = file_name |> Path.explode
    1.64      val _ = File.write path ""
    1.65 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.66      val ths =
    1.67 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    1.68 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.69        |> not include_thy ? filter_out (has_thy thy o snd)
    1.70        |> map snd
    1.71      val all_names = all_names ths
    1.72 @@ -116,8 +118,9 @@
    1.73      val path = file_name |> Path.explode
    1.74      val _ = File.write path ""
    1.75      val prover = hd provers
    1.76 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.77      val facts =
    1.78 -      all_facts_of (Proof_Context.init_global thy) Termtab.empty
    1.79 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.80        |> not include_thy ? filter_out (has_thy thy o snd)
    1.81      val ths = facts |> map snd
    1.82      val all_names = all_names ths
    1.83 @@ -134,8 +137,9 @@
    1.84      val path = file_name |> Path.explode
    1.85      val _ = File.write path ""
    1.86      val prover = hd provers
    1.87 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.88 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
    1.89 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.90 +    val facts =
    1.91 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
    1.92      val (new_facts, old_facts) =
    1.93        facts |> List.partition (has_thy thy o snd)
    1.94              |>> sort (thm_ord o pairself snd)
    1.95 @@ -164,8 +168,9 @@
    1.96      val path = file_name |> Path.explode
    1.97      val _ = File.write path ""
    1.98      val prover = hd provers
    1.99 -    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   1.100 -    val facts = all_facts_of (Proof_Context.init_global thy) css_table
   1.101 +    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   1.102 +    val facts =
   1.103 +      all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
   1.104      val (new_facts, old_facts) =
   1.105        facts |> List.partition (has_thy thy o snd)
   1.106              |>> sort (thm_ord o pairself snd)