# HG changeset patch
# User blanchet
# Date 1285571844 -7200
# Node ID b876d7525e7228ec11440858ff701812838ed880
# Parent  6e8c231876f59c830fc1b5833f66f85beaea30ed
comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)

diff -r 6e8c231876f5 -r b876d7525e72 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 27 09:14:39 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 27 09:17:24 2010 +0200
@@ -1980,9 +1980,11 @@
 *} "solve goal by normalization"
 
 
+(*
 subsection {* Try *}
 
 setup {* Try.setup *}
+*)
 
 subsection {* Counterexample Search Units *}
 
diff -r 6e8c231876f5 -r b876d7525e72 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Mon Sep 27 09:14:39 2010 +0200
+++ b/src/HOL/Tools/try.ML	Mon Sep 27 09:17:24 2010 +0200
@@ -2,18 +2,25 @@
     Author:     Jasmin Blanchette, TU Muenchen
 
 Try a combination of proof methods.
+
+FIXME: reintroduce or remove commented code (see also HOL.thy)
 *)
 
 signature TRY =
 sig
+(*
   val auto : bool Unsynchronized.ref
+*)
   val invoke_try : Time.time option -> Proof.state -> bool
+(*
   val setup : theory -> theory
+*)
 end;
 
 structure Try : TRY =
 struct
 
+(*
 val auto = Unsynchronized.ref false
 
 val _ =
@@ -21,6 +28,7 @@
   (Unsynchronized.setmp auto true (fn () =>
     Preferences.bool_pref auto
       "auto-try" "Try standard proof methods.") ());
+*)
 
 val default_timeout = Time.fromSeconds 5
 
@@ -108,8 +116,10 @@
       (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 setup = Auto_Tools.register_tool (tryN, auto_try)
+*)
 
 end;