src/HOL/Tools/try.ML
changeset 40301 bf39a257b3d3
parent 40222 cd6d2b0a4096
child 40931 061b8257ab9f
--- a/src/HOL/Tools/try.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/HOL/Tools/try.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -20,7 +20,7 @@
   ProofGeneralPgip.add_preference Preferences.category_tracing
       (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
 
-val default_timeout = Time.fromSeconds 5
+val default_timeout = seconds 5.0
 
 fun can_apply timeout_opt pre post tac st =
   let val {goal, ...} = Proof.goal st in