--- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
@@ -113,14 +113,12 @@
handle TYPE _ => @{prop True}
end
-fun all_non_tautological_facts_of ctxt prover thy css_table =
+fun all_non_tautological_facts_of thy css_table =
Sledgehammer_Fact.all_facts_of thy css_table
- |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology ctxt prover orf
- Sledgehammer_Filter_MaSh.is_too_meta) o snd)
+ |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
let
- val atp = atp_for_format format
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val type_enc =
type_enc |> type_enc_from_string Strict
@@ -128,7 +126,7 @@
val mono = not (is_type_enc_polymorphic type_enc)
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = all_non_tautological_facts_of ctxt atp thy css_table
+ val facts = all_non_tautological_facts_of thy css_table
val atp_problem =
facts
|> map (fn ((_, loc), th) =>