diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -852,7 +852,8 @@
   for the antiquotation @{text "term_pat"} is as follows.
 *}
 
-ML %linenosgray{*let
+ML %linenosgray{*val term_pat_setup = 
+let
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun term_pat (ctxt, str) =
@@ -860,9 +861,11 @@
          |> ML_Syntax.print_term
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline "term_pat" (parser >> term_pat)
+  ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
 end*}
 
+setup{* term_pat_setup *}
+
 text {*
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
@@ -878,7 +881,8 @@
   we can write an antiquotation for type patterns.
 *}
 
-ML{*let
+ML{*val type_pat_setup = 
+let
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun typ_pat (ctxt, str) =
@@ -886,9 +890,11 @@
          |> ML_Syntax.print_typ
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+  ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
 
+setup{* type_pat_setup *}
+
 text {*
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions