diff -r 3f85b675601c -r 0760fdf56942 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Jun 21 11:08:02 2012 +0100
+++ b/ProgTutorial/Essential.thy	Fri Jun 22 19:55:20 2012 +0100
@@ -12,7 +12,7 @@
   \end{flushright}
 
   \medskip
-  Isabelle is build around a few central ideas. One central idea is the
+  Isabelle is built around a few central ideas. One central idea is the
   LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
   is a small trusted core and everything else is built on top of this trusted
   core. The fundamental data structures involved in this core are certified
@@ -47,9 +47,11 @@
 
 text {*
   This datatype implements Church-style lambda-terms, where types are
-  explicitly recorded in variables, constants and abstractions.  As can be
-  seen in Line 5, terms use the usual de Bruijn index mechanism for
-  representing bound variables.  For example in
+  explicitly recorded in variables, constants and abstractions.  The
+  important point of having terms is that you can pattern-match against them;
+  this cannot be done with certified terms. 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]
   "@{term \"\<lambda>x y. x y\"}"
@@ -78,22 +80,33 @@
   with beta-redexes
 
   @{ML_response_fake [display, gray]
-"@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"}
-  |> pretty_term @{context}
-  |> pwriteln"
+"let 
+  val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
+  val arg1 = @{term \"1::int\"} 
+  val arg2 = @{term \"2::int\"}
+in
+  pretty_term @{context} (redex $ arg1 $ arg2)
+  |> pwriteln
+end"
   "1"}
 
-  There is a dedicated configuration value for switching off the tacit
-  eta-contraction, namely @{ML_ind eta_contract in Syntax} (see Section
+  There is a dedicated configuration value for switching off tacit
+  eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section
   \ref{sec:printing}), but none for beta-contractions. However you can avoid
-  the beta-contractions by switching off abbreviation using the configuration
+  the beta-contractions by switching off abbreviations using the configuration
   value @{ML_ind show_abbrevs in Syntax}. For example
 
 
   @{ML_response_fake [display, gray]
-  "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"}
-  |> pretty_term (Config.put show_abbrevs false @{context})
-  |> pwriteln"
+  "let 
+  val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
+  val arg1 = @{term \"1::int\"} 
+  val arg2 = @{term \"2::int\"}
+  val ctxt = Config.put show_abbrevs false @{context}
+in
+  pretty_term ctxt (redex $ arg1 $ arg2)
+  |> pwriteln
+end"
   "(\<lambda>x y. x) 1 2"}
 
   Isabelle makes a distinction between \emph{free} variables (term-constructor
@@ -195,7 +208,7 @@
   The corresponding datatype is
 *}
   
-ML_val{*datatype typ =
+ML_val %grayML{*datatype typ =
   Type  of string * typ list 
 | TFree of string * sort 
 | TVar  of indexname * sort *}