# HG changeset patch
# User blanchet
# Date 1335393180 -7200
# Node ID 7292038cad2ad35665a0d27ee21115b2ce655b51
# Parent  993a44ef99282dceaa974af5c63bdd19a170f717
tuning

diff -r 993a44ef9928 -r 7292038cad2a src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 26 00:29:46 2012 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 26 00:33:00 2012 +0200
@@ -22,7 +22,7 @@
 
 open Sledgehammer_Filter
 
-fun run_atp override_params relevance_override i n ctxt goal =
+fun run_prover override_params relevance_override i n ctxt goal =
   let
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
@@ -73,7 +73,7 @@
       override_params @
       [("preplay_timeout", "0")]
   in
-    case run_atp override_params relevance_override i i ctxt th of
+    case run_prover override_params relevance_override i i ctxt th of
       SOME facts =>
       Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
           (maps (thms_of_name ctxt) facts) i th
@@ -87,7 +87,7 @@
       override_params @
       [("preplay_timeout", "0"),
        ("minimize", "false")]
-    val xs = run_atp override_params relevance_override i i ctxt th
+    val xs = run_prover override_params relevance_override i i ctxt th
   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
 
 end;