tuned message;
authorwenzelm
Sat, 24 Jan 2015 21:36:21 +0100
changeset 59431 db440f97cf1a
parent 59430 b65809f05dc9
child 59432 42b7b76b37b8
tuned message;
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Jan 24 16:42:37 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Jan 24 21:36:21 2015 +0100
@@ -70,7 +70,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
-      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
+      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
         \(e.g., \"60\", \"0.5\") or \"none\".")
     else
       seconds (the secs)