1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Jul 25 11:26:23 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Jul 25 11:31:20 2014 +0200
     1.3 @@ -121,7 +121,8 @@
     1.4      end
     1.5    | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
     1.6    | Simp_Size_Method =>
     1.7 -    Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps @{thms size_ne_size_imp_ne})
     1.8 +    Simplifier.asm_full_simp_tac
     1.9 +      (silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
    1.10    | _ =>
    1.11      Method.insert_tac global_facts THEN'
    1.12      (case meth of