--- a/ProgTutorial/General.thy	Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/General.thy	Thu Nov 05 10:30:59 2009 +0100
@@ -362,9 +362,9 @@
 
   @{ML_response_fake [display,gray]
   "let
-  val app = Bound 0 $ Free (\"x\", @{typ nat})
+  val body = Bound 0 $ Free (\"x\", @{typ nat})
 in
-  Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, app)
+  Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
 end"
   "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
 
@@ -387,7 +387,7 @@
 text {*
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
-  "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual
+  "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual
   constructions of terms and types easier.
   \end{readmore}