src/HOL/ex/sledgehammer_tactics.ML
changeset 43021 5910dd009d0e
parent 43004 20e9caff1f86
child 43051 d7075adac3bd
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -23,7 +23,8 @@
     1.4         @ [("timeout", string_of_int (Time.toSeconds timeout))])
     1.5         (* @ [("overlord", "true")] *)
     1.6        |> Sledgehammer_Isar.default_params ctxt
     1.7 -    val prover = Sledgehammer_Provers.get_prover ctxt false name
     1.8 +    val prover =
     1.9 +      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    1.10      val default_max_relevant =
    1.11        Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    1.12      val is_built_in_const =