--- a/CookBook/FirstSteps.thy	Thu Jan 08 22:47:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sat Jan 10 12:57:48 2009 +0000
@@ -73,12 +73,12 @@
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
-  converting values into strings, for example:
+  converting values into strings, namely @{ML makestring}:
 
   @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} 
 
-  However this only works if the type of what is converted is monomorphic and is not 
-  a function.
+  However @{ML makestring} only works if the type of what is converted is monomorphic 
+  and is not a function.
 
   The function @{ML "warning"} should only be used for testing purposes, because any
   output this function generates will be overwritten as soon as an error is
@@ -89,7 +89,7 @@
   @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""}
 
   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
-  printed to a separate file, e.g. to prevent Proof General from choking on massive 
+  printed to a separate file, e.g. to prevent ProofGeneral from choking on massive 
   amounts of trace output. This redirection can be achieved using the code
 *}
 
@@ -159,7 +159,7 @@
   (FIXME: what does a simpset look like? It seems to be the same problem
   as with tokens.)
 
-  While antiquotations nowadays have many applications, they were originally introduced to 
+  While antiquotations have many applications, they were originally introduced to 
   avoid explicit bindings for theorems such as
 *}
 
@@ -228,14 +228,13 @@
   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
   Consider for example
 
-  @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"}
-  @{ML_response [display] "@{prop \"P x\"}" 
-                          "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"}
+  @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
+ Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
+ 
+  which inserts the coercion in the second component and 
 
-  which inserts the coercion in the latter case and 
-
-  @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
-  @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
+  @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
+  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 
   which does not (since it is already constructed using the meta-implication). 
 
@@ -255,7 +254,8 @@
 text {*
 
   While antiquotations are very convenient for constructing terms and types, 
-  they can only construct fixed terms. Unfortunately, one often needs to construct terms
+  they can only construct fixed terms (remember they are ``linked'' at compile-time). 
+  However, one often needs to construct terms
   dynamically. For example, a function that returns the implication 
   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
   as arguments can only be written as
@@ -265,16 +265,14 @@
 fun make_imp P Q tau =
   let
     val x = Free ("x",tau)
-  in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
-                                    HOLogic.mk_Trueprop (Q $ x)))
+  in Logic.all x (Logic.mk_implies (P $ x, Q $ x))
   end
 *}
 
 text {*
 
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example the following does not work as
-  expected.
+  @{term "tau"} into an antiquotation. For example the following does \emph{not} work:
 *}
 
 ML {*
@@ -283,7 +281,21 @@
 
 text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
-  to both functions. 
+  to both functions: 
+
+  @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" 
+    "Const \<dots> $ 
+    Abs (\"x\", Type (\"nat\",[]),
+      Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
+                  (Free (\"T\",\<dots>) $ \<dots>))"}
+  @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
+    "Const \<dots> $ 
+    Abs (\"x\", \<dots>,
+      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.
 
   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