diff -r 26d2f91608ed -r e11fe0de19a5 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri Jun 17 16:58:05 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Mon Jun 20 00:30:32 2011 +0100
@@ -192,8 +192,8 @@
   to separate them.
 *} 
 
-ML{*fun pretty_terms ctxt ts =  
-  Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*}
+ML{*fun pretty_terms ctxt trms =  
+  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 
 text {*
   You can also print out terms together with their typing information.
@@ -235,8 +235,8 @@
   A @{ML_type cterm} can be printed with the following function.
 *}
 
-ML{*fun pretty_cterm ctxt ct =  
-  pretty_term ctxt (term_of ct)*}
+ML{*fun pretty_cterm ctxt ctrm =  
+  pretty_term ctxt (term_of ctrm)*}
 
 text {*
   Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
@@ -244,8 +244,8 @@
   printed again with @{ML commas in Pretty}.
 *} 
 
-ML{*fun pretty_cterms ctxt cts =  
-  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) cts))*}
+ML{*fun pretty_cterms ctxt ctrms =  
+  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*}
 
 text {*
   The easiest way to get the string of a theorem is to transform it
@@ -284,7 +284,8 @@
   "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
-  Again the function @{ML commas} helps with printing more than one theorem. 
+  Again the functions @{ML commas} and @{ML block in Pretty} help 
+  with printing more than one theorem. 
 *}
 
 ML{*fun pretty_thms ctxt thms =  
@@ -294,7 +295,7 @@
   Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
 
 text {*
-  The printing functions for types are
+  Printing functions for types are
 *}
 
 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
@@ -313,7 +314,7 @@
   \begin{readmore}
   The simple conversion functions from Isabelle's main datatypes to 
   @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 
-  The references that change the printing information are declared in 
+  The configuration values that change the printing information are declared in 
   @{ML_file "Pure/Syntax/printer.ML"}.
   \end{readmore}
 
@@ -903,7 +904,8 @@
   data. Before we delve into the details, let us digress a bit. Conventional
   wisdom has it that the type-system of ML ensures that  an
   @{ML_type "'a list"}, say, can only hold elements of the same type, namely
-  @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a
+  @{ML_type "'a"} (or whatever is substitued for it). Despite this common 
+  wisdom, however, it is possible to implement a
   universal type in ML, although by some arguably accidental features of ML.
   This universal type can be used to store data of different type into a single list.
   In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is
@@ -976,6 +978,9 @@
   theories).  On the other hand, data such as facts change inside a proof and
   are only relevant to the proof at hand. Therefore such data needs to be 
   maintained inside a proof context, which represents ``local'' data.
+  You can think of a theory as the ``longterm memory'' of Isabelle (nothing will
+  be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically
+  changes according to what is needed at the time).
 
   For theories and proof contexts there are, respectively, the functors 
   @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help