adapted to strict pattern discipline

--- a/src/HOL/ex/NormalForm.thy	Wed Oct 29 11:33:40 2008 +0100
+++ b/src/HOL/ex/NormalForm.thy	Wed Oct 29 15:32:58 2008 +0100
@@ -34,7 +34,7 @@
   "add2 (S m) n = S(add2 m n)"
 
 declare add2.simps [code]
-lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
+lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
   by (induct n) auto
 lemma [code]: "add2 n (S m) =  S (add2 n m)"
   by(induct n) auto