--- a/ProgTutorial/First_Steps.thy	Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue Jul 08 11:34:10 2014 +0100
@@ -1,8 +1,7 @@
 theory First_Steps
 imports Base
 begin
-
-
+                                                  
 chapter {* First Steps\label{chp:firststeps} *}
 
 text {*
@@ -98,7 +97,7 @@
 
   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
-  will print out @{text [quotes] "any string"} inside the response buffer.  
+  will print out @{text [quotes] "any string"}.  
   This function expects a string as argument. If you develop under
   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
   for converting values into strings, namely the antiquotation 
@@ -114,11 +113,12 @@
 
   @{ML_response_fake [display,gray] 
   "if 0 = 1 then true else (error \"foo\")" 
-"Exception- ERROR \"foo\" raised
-At command \"ML\"."}
+"*** foo
+***"}
 
   This function raises the exception @{text ERROR}, which will then 
-  be displayed by the infrastructure. Note that this exception is meant 
+  be displayed by the infrastructure indicating that it is an error by
+  painting the output red. Note that this exception is meant 
   for ``user-level'' error messages seen by the ``end-user''. 
   For messages where you want to indicate a genuine program error, then
   use the exception @{text Fail}. 
@@ -152,7 +152,7 @@
 
 text {*
   You can also print out terms together with their typing information.
-  For this you need to set the configuration value 
+  For this you need to set the configuration value  
   @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 
@@ -543,7 +543,7 @@
   can be implemented more concisely as
 *}
 
-ML %grayML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate _ [] = ([], [])
   | separate i (x::xs) =
       if i <= x 
       then separate i xs ||> cons x
@@ -772,15 +772,17 @@
   difference between a theory and a context is will be described in Chapter
   \ref{chp:advanced}.) A context is for example needed in order to use the
   function @{ML print_abbrevs in Proof_Context} that list of all currently
-  defined abbreviations.
+  defined abbreviations. For example
 
   @{ML_response_fake [display, gray]
   "Proof_Context.print_abbrevs @{context}"
-"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
+"\<dots>
 INTER \<equiv> INFI
 Inter \<equiv> Inf
 \<dots>"}
 
+  The precise output of course depends on the abbreviations that are
+  currently defined; this can change over time.
   You can also use antiquotations to refer to proved theorems: 
   @{text "@{thm \<dots>}"} for a single theorem
 
@@ -812,14 +814,14 @@
   and the second is a proof. For example
 *}
 
-ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML %grayML{*val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
 
 text {*
   The result can be printed out as follows.
 
   @{ML_response_fake [gray,display]
-"foo_thm |> pretty_thms_no_vars @{context}
-        |> pwriteln"
+"foo_thms |> pretty_thms_no_vars @{context}
+         |> pwriteln"
   "True, False \<Longrightarrow> P"}
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
@@ -915,10 +917,9 @@
 
 setup %gray {* type_pat_setup *}
 
-text {*
-  However, a word of warning is in order: Introducing new antiquotations
-  should be done only after careful deliberations. They can make your 
-  code harder to read, than making it easier. 
+text {* 
+However, a word of warning is in order: Introducing new antiquotations should be done only after
+careful deliberations. They can potentially make your code harder to read, than making it easier.
 
   \begin{readmore}
   The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
@@ -992,10 +993,10 @@
   Notice that we access the integer as an integer and the boolean as
   a boolean. If we attempt to access the integer as a boolean, then we get 
   a runtime error. 
-  
+
   @{ML_response_fake [display, gray]
 "project_bool (nth foo_list 0)"  
-"*** Exception- Match raised"}
+"*** exception Match raised"}
 
   This runtime error is the reason why ML is still type-sound despite
   containing a universal type.
@@ -1216,7 +1217,7 @@
   for treating theories and proof contexts more uniformly. This type is defined as follows
 *}
 
-ML_val{*datatype generic = 
+ML_val %grayML{*datatype generic = 
   Theory of theory 
 | Proof of proof*}