# HG changeset patch
# User blanchet
# Date 1368632958 -7200
# Node ID 0c04e4c21eb3a8232f498acad9a7dfde64f45a8d
# Parent  f732a674db1be51e3ebab72a4b80c5b81f47be2d
compile

diff -r f732a674db1b -r 0c04e4c21eb3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 15 17:43:42 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed May 15 17:49:18 2013 +0200
@@ -451,9 +451,9 @@
           |> max_new_mono_instancesLST
           |> max_mono_itersLST)
     val default_max_facts =
-      Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover_name
+      Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
     val is_appropriate_prop =
-      Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
+      Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val time_limit =
       (case hard_timeout of
diff -r f732a674db1b -r 0c04e4c21eb3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed May 15 17:43:42 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed May 15 17:49:18 2013 +0200
@@ -116,13 +116,13 @@
          val params as {max_facts, slice, ...} =
            Sledgehammer_Isar.default_params ctxt args
          val default_max_facts =
-           Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover
+           Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover
          val is_appropriate_prop =
-           Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
+           Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt
                default_prover
          val relevance_fudge =
            extract_relevance_fudge args
-               (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
+               (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover