diff -r 069d525f8f1d -r ca0ac2e75f6d ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Mar 19 13:28:16 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Thu Mar 19 17:50:28 2009 +0100
@@ -1776,7 +1776,7 @@
   "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
 
   Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 
-  since the pretty-printer for @{ML_type cterm}s already beta-normalises terms.
+  since the pretty-printer for @{ML_type cterm}s eta-normalises terms.
   But how we constructed the term (using the function 
   @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
   ensures that the left-hand side must contain beta-redexes. Indeed
@@ -1810,8 +1810,7 @@
 end"
   "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"} 
 
-  Again, we actually see as output only the fully normalised term 
-  @{text "\<lambda>y. 2 + y"}.
+  Again, we actually see as output only the fully eta-normalised term.
 
   The main point of conversions is that they can be used for rewriting
   @{ML_type cterm}s. To do this you can use the function @{ML