# HG changeset patch
# User blanchet
# Date 1326130376 -3600
# Node ID 1148fab5104eda9e89c87b33012bb4f0a3d307bc
# Parent  e99ca055c91d252708ed0e98477b7d3d58cf27e0
revert unintended "sledgehammer" call

diff -r e99ca055c91d -r 1148fab5104e src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Jan 05 10:59:18 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Jan 09 18:32:56 2012 +0100
@@ -45,7 +45,6 @@
 nitpick [expect = none]
 nitpick [card 'a = 1\<emdash>50, expect = none]
 (* sledgehammer *)
-sledgehammer
 by (metis the_equality)
 
 subsection {* 2.4. Skolemization *}