--- a/ProgTutorial/FirstSteps.thy	Sat Oct 03 19:10:23 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Oct 04 21:56:53 2009 +0200
@@ -891,7 +891,7 @@
 
 text {*
   Using the injection functions, we can inject the integer @{ML_text "13"} 
-  and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and
+  and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and
   then store them in a @{ML_type "Universal.universal list"} as follows:
 *}
 
@@ -1003,7 +1003,7 @@
   there are no references involved. This is one of the most fundamental
   coding conventions for programming in Isabelle. References would 
   interfere with the multithreaded execution model of Isabelle and also
-  defeat the undo-mechanism in proof scripts. For this consider the 
+  defeat its undo-mechanism in proof scripts. For this consider the 
   following data container where we maintain a reference to a list of 
   integers.
 *}
@@ -1087,15 +1087,15 @@
   term and printing the list. 
 *}
 
-ML{*fun update trm = Data.map (fn xs => trm::xs)
+ML{*fun update trm = Data.map (fn trms => trm::trms)
 
 fun print ctxt =
   case (Data.get ctxt) of
     [] => tracing "Empty!"
-  | xs => tracing (string_of_terms ctxt xs)*}
+  | trms => tracing (string_of_terms ctxt trms)*}
 
 text {*
-  Next we start with the context given by the antiquotation 
+  Next we start with the context generated by the antiquotation 
   @{text "@{context}"} and update it in various ways. 
 
   @{ML_response_fake [display,gray]
@@ -1123,11 +1123,21 @@
   theory. Once we throw away the contexts, we have no access to their
   associated data. This is different to theories, where the command 
   \isacommand{setup} registers the data with the current and future 
-  theories, and therefore can access the data potentially 
+  theories, and therefore one can access the data potentially 
   indefinitely.\footnote{\bf FIXME: check this; it seems that is in
   conflict with the statements below.} 
 
-  \footnote{\bf FIXME: Say something about generic contexts.}
+  For convenience there is an abstract layer, the type @{ML_type Context.generic}, 
+  for theories and proof contexts. This type is defined as follows
+*}
+
+ML_val{*datatype generic = 
+  Theory of theory 
+| Proof of proof*}
+
+text {*
+  For this type a number of operations are defined which allow the
+  uniform treatment of theories and proof contexts.
 
   There are two special instances of the data storage mechanism described 
   above. The first instance are named theorem lists. Since storing theorems in a list