diff -r a5f53d9d2b60 -r f8537d69f514 doc-src/TutorialI/Misc/Plus.thy
--- a/doc-src/TutorialI/Misc/Plus.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Plus.thy	Thu May 29 22:45:33 2008 +0200
@@ -4,9 +4,8 @@
 
 text{*\noindent Define the following addition function *}
 
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-primrec
-"add m 0 = m"
+primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add m 0 = m" |
 "add m (Suc n) = add (Suc m) n"
 
 text{*\noindent and prove*}