1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 26 00:29:46 2012 +0200
1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 26 00:33:00 2012 +0200
1.3 @@ -22,7 +22,7 @@
1.4
1.5 open Sledgehammer_Filter
1.6
1.7 -fun run_atp override_params relevance_override i n ctxt goal =
1.8 +fun run_prover override_params relevance_override i n ctxt goal =
1.9 let
1.10 val chained_ths = [] (* a tactic has no chained ths *)
1.11 val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
1.12 @@ -73,7 +73,7 @@
1.13 override_params @
1.14 [("preplay_timeout", "0")]
1.15 in
1.16 - case run_atp override_params relevance_override i i ctxt th of
1.17 + case run_prover override_params relevance_override i i ctxt th of
1.18 SOME facts =>
1.19 Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
1.20 (maps (thms_of_name ctxt) facts) i th
1.21 @@ -87,7 +87,7 @@
1.22 override_params @
1.23 [("preplay_timeout", "0"),
1.24 ("minimize", "false")]
1.25 - val xs = run_atp override_params relevance_override i i ctxt th
1.26 + val xs = run_prover override_params relevance_override i i ctxt th
1.27 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
1.28
1.29 end;