src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 62826 eb94e570c1a4
parent 61432 1502f2410d8b
child 62969 9f394a16c557
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  fun parse_time name s =
     1.6    let val secs = if has_junk s then NONE else Real.fromString s in
     1.7 -    if is_none secs orelse Real.< (the secs, 0.0) then
     1.8 +    if is_none secs orelse the secs < 0.0 then
     1.9        error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
    1.10          \(e.g., \"60\", \"0.5\") or \"none\".")
    1.11      else