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