--- a/ProgTutorial/FirstSteps.thy	Thu Apr 02 12:19:11 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Fri Apr 03 07:55:07 2009 +0100
@@ -732,7 +732,7 @@
   "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
-  In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
+  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
   and an abstraction. It also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}