# HG changeset patch
# User blanchet
# Date 1391086452 -3600
# Node ID 03ac74b01e49e2083ed863b16839ee92d76404ef
# Parent  71cc2db86eec523dc9be343b9879394faba11636
compile

diff -r 71cc2db86eec -r 03ac74b01e49 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jan 30 13:39:57 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jan 30 13:54:12 2014 +0100
@@ -60,7 +60,7 @@
 (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
    bound exceeded" warnings and the like. *)
 fun silence_reconstructors debug =
-  Try0.silence_method debug
+  Try0.silence_methods debug
   #> Config.put SMT_Config.verbose debug
 
 end;