diff -r c8e9a4f97916 -r d563f8ff6aa0 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Sat Jan 10 12:57:48 2009 +0000
+++ b/CookBook/FirstSteps.thy	Mon Jan 12 16:03:05 2009 +0000
@@ -294,8 +294,9 @@
       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  As can be seen, in the first case the arguments are correctly used, while in the 
-  second the @{term "P"} and @{text "Q"} from the antiquotation.
+  As can be seen, in the first case the arguments are correctly used, while the 
+  second generates a term involving the @{term "P"} and @{text "Q"} from the 
+  antiquotation.
 
   One tricky point in constructing terms by hand is to obtain the 
   fully qualified name for constants. For example the names for @{text "zero"} and