--- a/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200
@@ -23,7 +23,8 @@
@ [("timeout", string_of_int (Time.toSeconds timeout))])
(* @ [("overlord", "true")] *)
|> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false name
+ val prover =
+ Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
val is_built_in_const =