--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 02 23:29:05 2016 +0200
@@ -460,7 +460,7 @@
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
- | Play_Timed_Out time => Time.> (time, Time.zeroTime)
+ | Play_Timed_Out time => time > Time.zeroTime
| Play_Failed => true)
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained