src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55308 dc68f6fb88d2
parent 55297 1dfcd49f5dcb
child 55323 253a029335a2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 23:20:12 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 23:38:33 2014 +0100
     1.3 @@ -77,7 +77,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 -> bool -> Time.time -> ((string * 'a) * thm) list ->
     1.8 +  val play_one_line_proof : mode -> 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 @@ -223,7 +223,7 @@
    1.13  fun filter_used_facts keep_chained used =
    1.14    filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
    1.15  
    1.16 -fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
    1.17 +fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
    1.18    let
    1.19      fun get_preferred meths = if member (op =) meths preferred then preferred else meth
    1.20    in