src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55286 7bbbd9393ce0
parent 55285 e88ad20035f4
child 55287 ffa306239316
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 15:19:07 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 15:33:18 2014 +0100
     1.3 @@ -215,10 +215,8 @@
     1.4      TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
     1.5    end
     1.6  
     1.7 -(* FIXME *)
     1.8 -fun timed_proof_method meth debug timeout ths =
     1.9 -  timed_apply timeout (silence_proof_methods debug
    1.10 -    #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
    1.11 +fun timed_proof_method meth timeout ths =
    1.12 +  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
    1.13  
    1.14  fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
    1.15  
    1.16 @@ -248,9 +246,9 @@
    1.17                    ()
    1.18                val timer = Timer.startRealTimer ()
    1.19              in
    1.20 -              case timed_proof_method meth debug timeout ths state i of
    1.21 +              (case timed_proof_method meth timeout ths state i of
    1.22                  SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
    1.23 -              | _ => play timed_out meths
    1.24 +              | _ => play timed_out meths)
    1.25              end
    1.26              handle TimeLimit.TimeOut => play (meth :: timed_out) meths
    1.27        in