--- a/ProgTutorial/Essential.thy	Sat Nov 21 00:29:43 2009 +0100
+++ b/ProgTutorial/Essential.thy	Sun Nov 22 03:13:29 2009 +0100
@@ -1169,7 +1169,8 @@
   complete typing annotations, especially in cases where the typing 
   information is redundant. A short-cut is to use the ``place-holder'' 
   type @{ML_ind dummyT in Term} and then let type-inference figure out the 
-  complete type. An example is as follows:
+  complete type. The type inference can be invoked with the function
+  @{ML_ind check_term in Syntax}. An example is as follows:
 
   @{ML_response_fake [display,gray] 
 "let
@@ -1325,7 +1326,7 @@
   |> implies_intr assm1
 end*}
 
-text {* 
+text {*
   If we print out the value of @{ML my_thm} then we see only the 
   final statement of the theorem.
 
@@ -1424,8 +1425,6 @@
 fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
 
 text {*
-  \footnote{\bf explain @{ML_ind add_thm in Thm} and @{ML_ind eq_thm_prop in Thm}.}
-
   The function @{ML update} allows us to update the theorem list, for example
   by adding the theorem @{thm [source] TrueI}.
 *}
@@ -1466,10 +1465,18 @@
   @{text "> True"}
   \end{isabelle}
 
-  There is a multitude of functions in the structures @{ML_struct Thm} and @{ML_struct Drule} 
-  for managing or manipulating theorems. For example 
-  we can test theorems for alpha equality. Suppose you proved the following three 
-  theorems.
+  Note that if we add the theorem @{thm [source] FalseE} again to the list
+*}
+
+setup %gray {* update @{thm FalseE} *}
+
+text {*
+  we still obtain the same list. The reason is that we used the function @{ML_ind
+  add_thm in Thm} in our update function. This is a dedicated function which
+  tests whether the theorem is already in the list.  This test is done
+  according to alpha-equivalence of the proposition behind the theorem. The
+  corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
+  Suppose you proved the following three theorems.
 *}
 
 lemma
@@ -1478,11 +1485,11 @@
   and   thm3: "\<forall>y. Q y" sorry
 
 text {*
-  Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces:
+  Testing them for alpha equality produces:
 
   @{ML_response [display,gray]
-"(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
- Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
+"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
+ Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
 "(true, false)"}
 
   Many functions destruct theorems into @{ML_type cterm}s. For example
@@ -1746,7 +1753,7 @@
   install this function as the theorem style named @{text "my_strip_allq"}. 
 *}
 
-setup %gray {*
+setup %gray{* 
   Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) 
 *}
 
@@ -1771,7 +1778,7 @@
 
   \begin{isabelle}
   @{text "@{thm (my_strip_allq) style_test}"}\\
-  @{text ">"}~@{thm (my_strip_allq) style_test}\\
+  @{text ">"}~@{thm (my_strip_allq) style_test}
   \end{isabelle}
   
   without the leading quantifiers. We can improve this theorem style by explicitly