diff -r 715163ec93c0 -r abfc66969d1f src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -8,15 +8,6 @@
 imports Main "~~/src/HOL/Real/Rational"
 begin
 
-lemma [code nbe]:
-  "x = x \<longleftrightarrow> True" by rule+
-
-lemma [code nbe]:
-  "eq_class.eq (x::bool) x \<longleftrightarrow> True" unfolding eq by rule+
-
-lemma [code nbe]:
-  "eq_class.eq (x::nat) x \<longleftrightarrow> True" unfolding eq by rule+
-
 lemma "True" by normalization
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
@@ -29,9 +20,6 @@
 
 datatype n = Z | S n
 
-lemma [code nbe]:
-  "eq_class.eq (x::n) x \<longleftrightarrow> True" unfolding eq by rule+
-
 consts
   add :: "n \<Rightarrow> n \<Rightarrow> n"
   add2 :: "n \<Rightarrow> n \<Rightarrow> n"
@@ -83,9 +71,6 @@
 lemma "[] @ xs = xs" by normalization
 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
 
-lemma [code nbe]:
-  "eq_class.eq (x :: 'a\<Colon>eq list) x \<longleftrightarrow> True" unfolding eq by rule+
-
 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
 lemma "rev [a, b, c] = [c, b, a]" by normalization
 normal_form "rev (a#b#cs) = rev cs @ [b, a]"