--- a/ProgTutorial/First_Steps.thy	Fri Nov 11 16:27:04 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Sat Nov 12 11:45:39 2011 +0000
@@ -669,13 +669,13 @@
 
 ML{*val (((one_def, two_def), three_def), ctxt') = 
   @{context}
-  |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
+  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
 
 text {*
-  where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
-  and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
+  where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"}
+  and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial
   context with the definitions. The result we are interested in is the
   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 
   information about the definitions---the function @{ML_ind add_def in Local_Defs} returns