diff -r e75614d0a859 -r b57f7fee72ee src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 21:08:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 22:23:26 2010 +0100
@@ -308,7 +308,7 @@
     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