src/HOL/Tools/try0.ML
changeset 58842 22b87ab47d3b
parent 58028 e4250d370657
child 58843 521cea5fa777
--- a/src/HOL/Tools/try0.ML	Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Oct 31 11:18:17 2014 +0100
@@ -22,13 +22,6 @@
 
 datatype mode = Auto_Try | Try | Normal;
 
-val _ =
-  ProofGeneral.preference_option ProofGeneral.category_tracing
-    NONE
-    @{system_option auto_methods}
-    "auto-try0"
-    "Try standard proof methods";
-
 val default_timeout = seconds 5.0;
 
 fun can_apply timeout_opt pre post tac st =