--- a/CookBook/FirstSteps.thy	Mon Oct 27 18:48:52 2008 +0100
+++ b/CookBook/FirstSteps.thy	Wed Oct 29 13:58:36 2008 +0100
@@ -8,7 +8,7 @@
 text {*
 
   Isabelle programming is done in Standard ML.
-  Just like lemmas and proofs, code in Isabelle is part of a 
+  Just like lemmas and proofs, SML-code in Isabelle is part of a 
   theory. If you want to follow the code written in this chapter, we 
   assume you are working inside the theory defined by
 
@@ -65,9 +65,6 @@
   \ldots
   \end{tabular}
   \end{center}
-
-  Note that from now on we are going to drop the 
-  \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. 
   
 *}
 
@@ -88,25 +85,26 @@
 
   @{ML [display] "warning (makestring 1)"} 
 
-  However this only works if the type of what is converted is monomorphic and not 
+  However this only works if the type of what is converted is monomorphic and is not 
   a function.
 
-  The funtion warning should only be used for testing purposes, because any
+  The funtion @{ML "warning"} should only be used for testing purposes, because any
   output this funtion generates will be overwritten, as soon as an error is
   raised. Therefore for printing anything more serious and elaborate, the
   function @{ML tracing} should be used. This function writes all output into
-  a separate buffer.
+  a separate tracing buffer.
 
   @{ML [display] "tracing \"foo\""}
 
   It is also possible to redirect the channel where the @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
   amounts of trace output. This rediretion can be achieved using the code
+*}
 
-@{ML_decl [display]
-"val strip_specials =
+ML {*
+val strip_specials =
 let
-  fun strip (\"\\^A\" :: _ :: cs) = strip cs
+  fun strip ("\^A" :: _ :: cs) = strip cs
     | strip (c :: cs) = c :: strip cs
     | strip [] = [];
 in implode o strip o explode end;
@@ -114,10 +112,13 @@
 fun redirect_tracing stream =
  Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
-     TextIO.output (stream, \"\\n\");
-     TextIO.flushOut stream));"}
+     TextIO.output (stream, "\n");
+     TextIO.flushOut stream));
+*}
 
-  Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
+text {*
+
+  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
 *}
@@ -141,14 +142,18 @@
 
   Note, however, that antiquotations are statically scoped, that is the value is
   determined at ``compile-time'', not ``run-time''. For example the function
+*}
 
-  @{ML_decl [display]
-  "fun not_current_thyname () = Context.theory_name @{theory}"}
+ML {*
+fun not_current_thyname () = Context.theory_name @{theory}
+*}
+
+text {*
 
   does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
   that always returns the string @{ML_text "FirstSteps"}, no matter where the
-  function is called. Operationally speaking,  @{text "@{theory}"} is 
+  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
   \emph{not} replaced with code that will look up the current theory in 
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
@@ -158,7 +163,20 @@
   @{ML [display] "@{thm allI}"}
   @{ML [display] "@{simpset}"}
 
-  In the course of this introduction, we will learn more about 
+  While antiquotations have many uses, they were introduced to avoid explicit
+  bindings for theorems such as
+*}
+
+ML {*
+val allI = thm "allI"
+*}
+
+text {*
+  These bindings were difficult to maintain and also could be overwritten
+  by bindings introduced by the user. This had the potential to break
+  definitional packages. This additional layer of maintenance complexity
+  can be avoided by using antiquotations, since they are ``linked'' statically
+  at compile time.  In the course of this introduction, we will learn more about 
   these antiquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
 
@@ -257,20 +275,28 @@
   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 typ @{term "\<tau>"}
   as arguments can only be written as
+*}
 
-@{ML_decl [display]
-"fun make_imp P Q tau =
+ML {*
+fun make_imp P Q tau =
   let
-    val x = Free (\"x\",tau)
+    val x = Free ("x",tau)
   in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
                                     HOLogic.mk_Trueprop (Q $ x)))
-  end"}
+  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.
+*}
 
-  @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\<And>x. P x \<Longrightarrow> Q x\"}"} 
+ML {*
+fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
+*}
 
+text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
   to both functions.