1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:19:07 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:33:18 2014 +0100
     1.3 @@ -284,9 +284,7 @@
     1.4            |> postprocess_isar_proof_remove_unreferenced_steps I
     1.5            |> relabel_isar_proof_canonically
     1.6  
     1.7 -        val ctxt = ctxt
     1.8 -          |> enrich_context_with_local_facts canonical_isar_proof
     1.9 -          |> silence_proof_methods debug
    1.10 +        val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
    1.11  
    1.12          val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
    1.13