
diff -r 056255ade52a -r 4e74209f113e src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -12,7 +12,7 @@
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-declare disj_assoc [code func del]
+declare disj_assoc [code del]
 lemma "0 + (n::nat) = n" by normalization
 lemma "0 + Suc n = Suc n" by normalization
 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization




