--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Nov 20 00:53:26 2010 +0100
@@ -313,7 +313,7 @@
val digit = Scan.one Symbol.is_ascii_digit;
val num3 = as_num (digit ::: digit ::: (digit >> single));
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
- val as_time = Scan.read Symbol.stopper time o explode
+ val as_time = Scan.read Symbol.stopper time o raw_explode
in (output, as_time t) end;
fun run_on probfile =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of