# HG changeset patch
# User wenzelm
# Date 1415282715 -3600
# Node ID ffdafc99f67be22b3d2e357dfd8cc3e689427caf
# Parent  2f8168dc0eac5bdcde73fbf39293d883034161ff
prefer explicit Keyword.keywords (cf. 82a71046dce8);

diff -r 2f8168dc0eac -r ffdafc99f67b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r 2f8168dc0eac -r ffdafc99f67b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- 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
diff -r 2f8168dc0eac -r ffdafc99f67b src/HOL/TPTP/sledgehammer_tactics.ML
--- 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