--- a/ProgTutorial/First_Steps.thy	Sun Oct 30 17:45:10 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Wed Nov 02 13:38:19 2011 +0000
@@ -508,9 +508,10 @@
 
 text {*
   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
-  @{ML_ind note in Local_Theory}; its purpose is to store a theorem under a name. 
-  In lines 5 to 6 we call this function to give alternative names for three
-  theorems. The point of @{ML "#>"} is that you can sequence such functions. 
+  @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; 
+  its purpose is to store a theorem under a name. 
+  In lines 5 to 6 we call this function to give alternative names for the three
+  theorems. The point of @{ML "#>"} is that you can sequence such function calls. 
 
   The remaining combinators we describe in this section add convenience for
   the ``waterfall method'' of writing functions. The combinator @{ML_ind tap