--- a/ProgTutorial/FirstSteps.thy	Wed Jun 24 15:58:59 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 14 01:42:35 2009 +0200
@@ -57,7 +57,7 @@
   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 
+  `ambient' theory is suppressed. The second needs to be used if ML-code is defined 
   inside a proof. For example
 
   \begin{quote}
@@ -69,8 +69,8 @@
   \end{isabelle}
   \end{quote}
 
-  However, both commands will not play any role in this tutorial (we, for example, 
-  always assume the ML-code is defined outside proofs).
+  However, both commands will only play minor roles in this tutorial (we will always 
+  arrange that the ML-code is defined outside of proofs).
 
   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 
@@ -102,7 +102,11 @@
   \end{tabular}
   \end{quote}
 
-  Note that no parentheses are given this time. 
+  Note that no parentheses are given this time. Note also that the 
+  `used' 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.
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
@@ -230,12 +234,12 @@
 
   In order to improve the readability of theorems we convert
   these schematic variables into free variables using the 
-  function @{ML [index] import_thms in Variable}.
+  function @{ML [index] import in Variable}.
 *}
 
 ML{*fun no_vars ctxt thm =
 let 
-  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+  val ((_, [thm']), _) = Variable.import true [thm] ctxt
 in
   thm'
 end
@@ -630,6 +634,26 @@
   kinds of logical elements from the ML-level.
 *}
 
+text {* FIXME: 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))*}
+
+ML{*@{term_pat "?x + ?y"}*}
+
+text {*
+
+  \begin{readmore}
+  @{ML_file "Pure/ML/ml_antiquote.ML"}
+  \end{readmore}
+*}
+
 section {* Terms and Types *}
 
 text {*
@@ -1700,9 +1724,7 @@
   @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 
   \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
-  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
-  data.
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
   \end{readmore}
 
   (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)