# HG changeset patch
# User blanchet
# Date 1406280680 -7200
# Node ID 3bad83e01ec2d26398baa731dd5927bc34f903b3
# Parent  858c1a63967fe75cc1cef83345045792cff6ad5e
added missing facts to proof method

diff -r 858c1a63967f -r 3bad83e01ec2 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- 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