# 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