--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Nov 20 00:53:26 2010 +0100
@@ -444,7 +444,7 @@
val (prover_name, _) = get_prover ctxt args
val timeout =
AList.lookup (op =) args minimize_timeoutK
- |> Option.map (fst o read_int o explode)
+ |> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),