# HG changeset patch
# User wenzelm
# Date 1634114101 -7200
# Node ID a241eadc0e3fec75b74bb8c984ae75946f00c13a
# Parent  d97c48dc87fa4cf898b9427abe6a94eeec0ebc5d
removed unused material (left-over from fd0c85d7da38);

diff -r d97c48dc87fa -r a241eadc0e3f src/Tools/try.ML
--- a/src/Tools/try.ML	Wed Oct 13 00:07:06 2021 +0200
+++ b/src/Tools/try.ML	Wed Oct 13 10:35:01 2021 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Tools/try.ML
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Makarius
 
 Manager for tools that should be tried on conjectures.
 *)
@@ -78,19 +79,7 @@
     (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)));
 
 
-(* automatic try (TTY) *)
-
-fun auto_try state =
-  get_tools (Proof.theory_of state)
-  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
-  |> Par_List.get_some (fn tool =>
-    (case try (tool true) state of
-      SOME (true, (_, outcome)) => SOME outcome
-    | _ => NONE))
-  |> the_default [];
-
-
-(* asynchronous print function (PIDE) *)
+(* asynchronous print function *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
   Command.print_function ("auto_" ^ name)