--- a/ProgTutorial/Essential.thy	Wed Feb 15 14:52:03 2012 +0000
+++ b/ProgTutorial/Essential.thy	Sun Feb 19 01:33:47 2012 +0000
@@ -1470,10 +1470,10 @@
 
   Since certified terms are, unlike terms, abstract objects, we cannot
   pattern-match against them. However, we can construct them. For example
-  the function @{ML_ind capply in Thm} produces a certified application.
+  the function @{ML_ind apply in Thm} produces a certified application.
 
   @{ML_response_fake [display,gray]
-  "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
+  "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
   "P 3"}
 
   Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}