--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 14 14:12:18 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 14 14:22:49 2010 +0200
@@ -38,8 +38,7 @@
lemma "P x \<Longrightarrow> P (THE y. P y)"
nitpick [show_consts, expect = genuine]
-nitpick [full_descrs, show_consts, expect = genuine]
-nitpick [dont_specialize, full_descrs, show_consts, expect = genuine]
+nitpick [dont_specialize, show_consts, expect = genuine]
oops
lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"