--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 02 23:29:05 2016 +0200
@@ -541,7 +541,7 @@
val facts = named_thms |> map (ref_of_str o fst o fst)
val fact_override = {add = facts, del = [], only = true}
fun my_timeout time_slice =
- timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
+ timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal
fun sledge_tac time_slice prover type_enc =
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
(override_params prover type_enc (my_timeout time_slice)) fact_override []