proper Keyword.keywords (cf. 82a71046dce8);
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Nov 06 15:05:15 2014 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Nov 06 15:42:34 2014 +0100
@@ -165,7 +165,7 @@
val mono = not (is_type_enc_polymorphic type_enc)
val facts =
Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
- Symtab.empty [] [] css_table
+ Keyword.empty_keywords [] [] css_table
|> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
val problem =
facts
--- a/src/HOL/TPTP/mash_eval.ML Thu Nov 06 15:05:15 2014 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Nov 06 15:42:34 2014 +0100
@@ -53,7 +53,7 @@
val liness' = Ctr_Sugar_Util.transpose (map pad liness0)
val css = clasimpset_rule_table_of ctxt
- val facts = all_facts ctxt true false Symtab.empty [] [] css
+ val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
--- a/src/HOL/TPTP/mash_export.ML Thu Nov 06 15:05:15 2014 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Nov 06 15:42:34 2014 +0100
@@ -64,7 +64,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
+ Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
|> sort (crude_thm_ord o pairself snd)
end