--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri May 28 22:34:21 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri May 28 22:51:04 2010 +0200
@@ -638,14 +638,6 @@
nitpick [expect = none]
by (simp add: snd_def)
-lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
-nitpick [expect = none]
-by (simp add: fst_def)
-
-lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
-nitpick [expect = none]
-by (simp add: snd_def)
-
lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
nitpick [expect = none]
by auto