src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 62826 eb94e570c1a4
parent 62738 fe827c6fa8c5
child 62969 9f394a16c557
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4          val facts = named_thms |> map (ref_of_str o fst o fst)
     1.5          val fact_override = {add = facts, del = [], only = true}
     1.6          fun my_timeout time_slice =
     1.7 -          timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
     1.8 +          timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal
     1.9          fun sledge_tac time_slice prover type_enc =
    1.10            Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.11              (override_params prover type_enc (my_timeout time_slice)) fact_override []