src/HOL/ex/sledgehammer_tactics.ML
changeset 42444 8e5438dc70bb
parent 42443 724e612ba248
child 42449 494e4ac5b0f8
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     1.3 @@ -23,7 +23,7 @@
     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 true name
     1.8 +    val prover = Sledgehammer_Provers.get_prover ctxt false name
     1.9      val default_max_relevant =
    1.10        Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    1.11      val is_built_in_const =