diff -r bd27ac6ad1c3 -r e88ad20035f4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -286,7 +286,7 @@
 
         val ctxt = ctxt
           |> enrich_context_with_local_facts canonical_isar_proof
-          |> silence_reconstructors debug
+          |> silence_proof_methods debug
 
         val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
@@ -354,9 +354,9 @@
           if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
   in one_line_proof ^ isar_proof end
 
-fun isar_proof_would_be_a_good_idea (reconstr, play) =
+fun isar_proof_would_be_a_good_idea (meth, play) =
   (case play of
-    Played _ => reconstr = SMT
+    Played _ => meth = SMT_Method
   | Play_Timed_Out _ => true
   | Play_Failed => true
   | Not_Played => false)