--- a/ProgTutorial/FirstSteps.thy	Thu May 28 12:15:50 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri May 29 12:15:48 2009 +0200
@@ -54,20 +54,22 @@
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
   show code. The lines prefixed with @{text [quotes] ">"} are not part of the
   code, rather they indicate what the response is when the code is evaluated.
-  There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf}.
-  The first evaluates the given code, but any effect on the ambient
-  theory is suppressed. The second needs to be used if ML-code is defined 
+  There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
+  including ML-code. The first evaluates the given code, but any effect on the 
+  ambient theory is suppressed. The second needs to be used if ML-code is defined 
   inside a proof. For example
 
-\begin{isabelle}
-\isacommand{lemma}~@{text "test:"}\isanewline
-\isacommand{shows}~@{text [quotes] "True"}\isanewline
-\isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial\""}~@{text "\<verbclose>"}\isanewline
-\isacommand{oops}
-\end{isabelle}
+  \begin{quote}
+  \begin{isabelle}
+  \isacommand{lemma}~@{text "test:"}\isanewline
+  \isacommand{shows}~@{text [quotes] "True"}\isanewline
+  \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline
+  \isacommand{oops}
+  \end{isabelle}
+  \end{quote}
 
-  Inside a proof the \isacommand{ML} will generate an error message.
-  However, both commands will not play any role in this tutorial.
+  However, both commands will not play any role in this tutorial (we, for example, 
+  always assume the ML-code is defined outside proofs).
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
@@ -99,7 +101,7 @@
   \end{tabular}
   \end{quote}
 
-  Note that no parentheses are given this time.
+  Note that no parentheses are given this time. 
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
@@ -639,7 +641,7 @@
   representation corresponding to the datatype @{ML_type "term"} defined as follows: 
 *}  
 
-ML_val{*datatype term =
+ML_val %linenosgray{*datatype term =
   Const of string * typ 
 | Free of string * typ 
 | Var of indexname * typ 
@@ -648,8 +650,8 @@
 | $ of term * term *}
 
 text {*
-  Terms use the usual de Bruijn index mechanism---where
-  bound variables are represented by the constructor @{ML Bound}.  For
+  As can be seen in Line 5, terms use the usual de Bruijn index mechanism
+  for representing bound variables.  For
   example in
 
   @{ML_response_fake [display, gray]
@@ -686,12 +688,14 @@
 
   When constructing terms, you are usually concerned with free variables (for example
   you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 
-  If you deal with theorems, you have to observe the distinction. A similar
+  If you deal with theorems, you have to, however, observe the distinction. A similar
   distinction holds for types (see below).
 
   \begin{readmore}
   Terms and types are described in detail in \isccite{sec:terms}. Their
   definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
+  For constructing terms involving HOL constants, many helper functions are defined
+  in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
   
   Constructing terms via antiquotations has the advantage that only typable