src/HOL/Sledgehammer.thy

--- a/src/HOL/Sledgehammer.thy	Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Dec 20 20:36:38 2013 +0100
@@ -11,6 +11,9 @@
 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 begin
 
+lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
+by (erule contrapos_nn) (rule arg_cong)
+
 ML_file "Tools/Sledgehammer/async_manager.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"