diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/TutorialI/Misc/Option2.thy
--- a/doc-src/TutorialI/Misc/Option2.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Misc/Option2.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -24,8 +24,7 @@
 *}
 (*<*)
 (*
-constdefs
- infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option"
+definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where
 "infplus x y \<equiv> case x of None \<Rightarrow> None
                | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"