--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Dec 20 20:36:38 2013 +0100
@@ -97,6 +97,8 @@
Method.insert_tac facts THEN'
(case meth of
Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
| Auto_Method => K (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
| Force_Method => Clasimp.force_tac ctxt