prefer explicit Keyword.keywords (cf. 82a71046dce8);

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 06 13:44:14 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 06 15:05:15 2014 +0100
@@ -414,11 +414,11 @@
          time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
         val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
-        val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
+        val keywords = Keyword.get_keywords ()
         val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
         val facts =
           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-              Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
+              Sledgehammer_Fact.no_fact_override keywords css_table chained_ths
               hyp_ts concl_t
         val factss =
           facts

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Nov 06 13:44:14 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Nov 06 15:05:15 2014 +0100
@@ -110,11 +110,11 @@
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
          val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover
-         val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
+         val keywords = Keyword.get_keywords ()
          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
          val facts =
            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-               Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
+               Sledgehammer_Fact.no_fact_override keywords css_table chained_ths
                hyp_ts concl_t
            |> Sledgehammer_Fact.drop_duplicate_facts
            |> Sledgehammer_MePo.mepo_suggested_facts ctxt params

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Nov 06 13:44:14 2014 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Nov 06 15:05:15 2014 +0100
@@ -36,10 +36,10 @@
     val default_max_facts = default_max_facts_of_prover ctxt name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val ho_atp = exists (is_ho_atp ctxt) provers
-    val reserved = reserved_isar_keyword_table ()
+    val keywords = Keyword.get_keywords ()
     val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      nearly_all_facts ctxt ho_atp fact_override reserved css_table chained hyp_ts concl_t
+      nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
       |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
         hyp_ts concl_t
       |> hd |> snd