--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Apr 02 23:29:05 2016 +0200
@@ -69,7 +69,7 @@
fun parse_time name s =
let val secs = if has_junk s then NONE else Real.fromString s in
- if is_none secs orelse Real.< (the secs, 0.0) then
+ if is_none secs orelse the secs < 0.0 then
error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
\(e.g., \"60\", \"0.5\") or \"none\".")
else