# HG changeset patch
# User wenzelm
# Date 1415284954 -3600
# Node ID 1f500b18c4c6841aca732b34f5e1078318400e73
# Parent  ffdafc99f67be22b3d2e357dfd8cc3e689427caf
proper Keyword.keywords (cf. 82a71046dce8);

diff -r ffdafc99f67b -r 1f500b18c4c6 src/HOL/TPTP/atp_theory_export.ML
--- 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
diff -r ffdafc99f67b -r 1f500b18c4c6 src/HOL/TPTP/mash_eval.ML
--- 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)
diff -r ffdafc99f67b -r 1f500b18c4c6 src/HOL/TPTP/mash_export.ML
--- 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