# HG changeset patch
# User wenzelm
# Date 1380021805 -7200
# Node ID 274a892b1230c279ab1a0e793a1f3e4bc8b36105
# Parent  b9285f30a80ac1a74cc4846a214a1cfe59b5b04e
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);

diff -r b9285f30a80a -r 274a892b1230 src/Tools/try.ML
--- a/src/Tools/try.ML	Tue Sep 24 11:28:18 2013 +0200
+++ b/src/Tools/try.ML	Tue Sep 24 13:23:25 2013 +0200
@@ -116,7 +116,7 @@
 (* asynchronous print function (PIDE) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
-  Command.print_function name
+  Command.print_function ("auto_" ^ name)
     (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME