src/HOL/Tools/try.ML
changeset 40931 061b8257ab9f
parent 40301 bf39a257b3d3
child 41038 9592334001d5
--- a/src/HOL/Tools/try.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/try.ML	Fri Dec 03 09:55:45 2010 +0100
@@ -110,8 +110,8 @@
       (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
                                     o Toplevel.proof_of)))
 
-fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
+val auto_try = do_try true NONE
 
-val setup = Auto_Tools.register_tool (tryN, auto_try)
+val setup = Auto_Tools.register_tool (auto, auto_try)
 
 end;