--- a/ProgTutorial/FirstSteps.thy	Sat Apr 25 17:46:47 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Apr 26 23:45:22 2009 +0200
@@ -5,8 +5,7 @@
 chapter {* First Steps *}
 
 text {*
-
-  Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
+  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
 
@@ -890,6 +889,12 @@
   | is_nil_or_all _ = false *}
 
 text {*
+  The antiquotation for properly referencing type constants is  is @{text "@{type_name \<dots>}"}.
+  For example
+
+  @{ML_response [display,gray]
+  "@{type_name \"list\"}" "\"List.list\""}
+
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
   @{ML Long_Name.base_name}. For example: