# HG changeset patch
# User wenzelm
# Date 1422131781 -3600
# Node ID db440f97cf1af8c878d2d087ec185977a5ea8e35
# Parent  b65809f05dc9236601a3c2c1720b95ae17528f57
tuned message;

diff -r b65809f05dc9 -r db440f97cf1a 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)