src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55452 29ec8680e61f
parent 55345 8a53ee72e595
child 55453 0b070d098d1a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4    val filter_used_facts :
     1.5      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     1.6      ((''a * stature) * 'b) list
     1.7 -  val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
     1.8 +  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
     1.9      Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
    1.10    val remotify_atp_if_not_installed : theory -> string -> string option
    1.11    val isar_supported_prover_of : theory -> string -> string
    1.12 @@ -219,15 +219,15 @@
    1.13      TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
    1.14    end
    1.15  
    1.16 -fun timed_proof_method meth timeout ths =
    1.17 -  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
    1.18 +fun timed_proof_method debug timeout ths meth =
    1.19 +  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
    1.20  
    1.21  fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
    1.22  
    1.23  fun filter_used_facts keep_chained used =
    1.24    filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
    1.25  
    1.26 -fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
    1.27 +fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
    1.28    let
    1.29      fun get_preferred meths = if member (op =) meths preferred then preferred else meth
    1.30    in
    1.31 @@ -249,7 +249,7 @@
    1.32                    ()
    1.33                val timer = Timer.startRealTimer ()
    1.34              in
    1.35 -              (case timed_proof_method meth timeout ths state i of
    1.36 +              (case timed_proof_method debug timeout ths meth state i of
    1.37                  SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
    1.38                | _ => play timed_out meths)
    1.39              end