--- a/ProgTutorial/FirstSteps.thy	Sat Nov 07 01:44:11 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sat Nov 07 10:08:09 2009 +0100
@@ -275,7 +275,7 @@
   where @{text 1} and @{text x} are displayed with their inferred type.
   Even more type information can be printed by setting 
   the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
-  We obtain then
+  In this case we obtain
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
@@ -285,8 +285,8 @@
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
   where @{term Pair} is the term-constructor for products. 
-  Other references that influence printing are @{ML_ind show_brackets in Syntax} 
-  and @{ML_ind show_sorts in Syntax}. 
+  Other references that influence printing of terms are 
+  @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. 
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)
@@ -774,7 +774,7 @@
 *}
 
 
-section {* ML-Antiquotations *}
+section {* ML-Antiquotations\label{sec:antiquote} *}
 
 text {*
   Recall from Section \ref{sec:include} that code in Isabelle is always
@@ -845,11 +845,11 @@
 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *}
 
 text {*
-  which can be printed out as follows
+  The result can be printed out as follows.
 
   @{ML_response_fake [gray,display]
 "foo_thm |> string_of_thms @{context}
-         |> tracing"
+        |> tracing"
   "True, True"}
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
@@ -949,8 +949,22 @@
   "@{term_pat \"Suc (?x::nat)\"}"
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
-  which shows the internal representation of the term @{text "Suc ?x"}.
+  which shows the internal representation of the term @{text "Suc ?x"}. Similarly
+  we can write an antiquotation for type patterns.
+*}
+
+ML %linenosgray{*let
+  val parser = Args.context -- Scan.lift Args.name_source
 
+  fun typ_pat (ctxt, str) =
+     str |> Syntax.parse_typ ctxt
+         |> ML_Syntax.print_typ
+         |> ML_Syntax.atomic
+in
+  ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+end*}
+
+text {*
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
   for most antiquotations. Most of the basic operations on ML-syntax are implemented 
@@ -1267,8 +1281,8 @@
 text {*
   This code declares a data container where the theorems are stored,
   an attribute @{text foo} (with the @{text add} and @{text del} options
-  for adding and deleting theorems) and an internal ML-interface to retrieve and 
-  modify the theorems.
+  for adding and deleting theorems) and an internal ML-interface for retrieving and 
+  modifying the theorems.
   Furthermore, the theorems are made available on the user-level under the name 
   @{text foo}. For example you can declare three lemmas to be a member of the 
   theorem list @{text foo} by: