src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 40627 becf5d5187cc
parent 40554 ff446d5e9a62
child 40667 b8579f24ce67
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -444,7 +444,7 @@
     1.4      val (prover_name, _) = get_prover ctxt args
     1.5      val timeout =
     1.6        AList.lookup (op =) args minimize_timeoutK
     1.7 -      |> Option.map (fst o read_int o explode)
     1.8 +      |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
     1.9        |> the_default 5
    1.10      val params = Sledgehammer_Isar.default_params ctxt
    1.11        [("verbose", "true"),