src/HOL/Tools/SMT/smt_solver.ML

   let
     val {facts, goal, ...} = Proof.goal st
     val ctxt =
       Proof.context_of st
       |> Config.put C.oracle false
-      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
+      |> Config.put C.timeout (Time.toReal time_limit)
       |> Config.put C.drop_bad_facts true
       |> Config.put C.filter_only_facts true
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     val cprop =
       concl