diff -r 195c4444dff7 -r 311830b43f8f ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Jul 14 01:42:35 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 14 16:34:24 2009 +0200
@@ -57,7 +57,8 @@
   code, rather they indicate what the response is when the code is evaluated.
   There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
   including ML-code. The first evaluates the given code, but any effect on the 
-  `ambient' theory is suppressed. The second needs to be used if ML-code is defined 
+  theory, in which the code is embedded, is suppressed. The second needs to 
+  be used if ML-code is defined 
   inside a proof. For example
 
   \begin{quote}
@@ -70,7 +71,7 @@
   \end{quote}
 
   However, both commands will only play minor roles in this tutorial (we will always 
-  arrange that the ML-code is defined outside of proofs).
+  arrange that the ML-code is defined outside of proofs, for example).
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a 
@@ -103,7 +104,7 @@
   \end{quote}
 
   Note that no parentheses are given this time. Note also that the 
-  `used' file should not contain any
+  included ML-file should not contain any
   \isacommand{use} itself. Otherwise Isabelle is unable to record all
   file dependencies, which is a nuisance if you have to track down
   errors.
@@ -634,21 +635,18 @@
   kinds of logical elements from the ML-level.
 *}
 
-text {* FIXME: an example of a user defined antiquotation *}
+text {* FIXME: give an example of a user defined antiquotation *}
 
 ML{*ML_Antiquote.inline "term_pat"
   (Args.context -- Scan.lift Args.name_source >>
      (fn (ctxt, s) =>
-       let 
-         val t = ProofContext.read_term_pattern ctxt s
-       in 
-         ML_Syntax.atomic (ML_Syntax.print_term t) 
-       end))*}
+       s |> ProofContext.read_term_pattern ctxt
+         |> ML_Syntax.print_term
+         |> ML_Syntax.atomic))*}
 
 ML{*@{term_pat "?x + ?y"}*}
 
 text {*
-
   \begin{readmore}
   @{ML_file "Pure/ML/ml_antiquote.ML"}
   \end{readmore}