# HG changeset patch
# User haftmann
# Date 1225290778 -3600
# Node ID 6a5d214aaa8255250189b3a03d16e29025800171
# Parent  a1a436f09ec6c6e24a20bcccb3feec72f3357e39
adapted to strict pattern discipline

diff -r a1a436f09ec6 -r 6a5d214aaa82 src/HOL/ex/NormalForm.thy
--- 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