src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 40627 becf5d5187cc
parent 40562 bbcb7aa90afc
child 40666 8db6c2b1591d
--- 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