# HG changeset patch
# User blanchet
# Date 1364893131 -7200
# Node ID 89bfe7a336152f869df12f10a22f74334e359922
# Parent  d40aec502416a0eaa094e5aef1f317f7c4867852
got rid of legacy smartness

diff -r d40aec502416 -r 89bfe7a33615 src/Tools/try.ML
--- a/src/Tools/try.ML	Mon Apr 01 17:42:29 2013 +0200
+++ b/src/Tools/try.ML	Tue Apr 02 10:58:51 2013 +0200
@@ -104,19 +104,9 @@
                            | _ => NONE)
   |> the_default state
 
-(* Too large values are understood as milliseconds, ensuring compatibility with
-   old setting files. No users can possibly in their right mind want the user
-   interface to block for more than 100 seconds. *)
-fun smart_seconds r =
-  seconds (if r >= 100.0 then
-             (legacy_feature (quote auto_try_time_limitN ^
-                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
-           else
-             r)
-
 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
-    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
+    TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state
     handle TimeLimit.TimeOut => state
   else
     state))