diff -r a5f53d9d2b60 -r f8537d69f514 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Thu May 29 22:45:33 2008 +0200
@@ -45,10 +45,9 @@
 gradually, using only~@{text"#"}:
 *}
 
-consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
-primrec
-"itrev []     ys = ys"
-"itrev (x#xs) ys = itrev xs (x#ys)";
+primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev []     ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
 
 text{*\noindent
 The behaviour of \cdx{itrev} is simple: it reverses