diff -r 4cc6df387ce9 -r 8ad407e77ea0 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Sun Nov 15 13:47:31 2009 +0100
+++ b/ProgTutorial/Intro.thy	Tue Nov 17 18:40:11 2009 +0100
@@ -194,6 +194,7 @@
   \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
   \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
   \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
+  \item @{text "S"} for sorts; ML-type: @{ML_type sort}
   \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
   \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
   \item @{text thy} for theories; ML-type: @{ML_type theory}
@@ -226,6 +227,9 @@
   and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
   are by him.
 
+  \item {\bf Lukas Bulwahn} made me aware of the problems with recursive
+  parsers.
+
   \item {\bf Jeremy Dawson} wrote the first version of the chapter
   about parsing.
 
@@ -255,6 +259,4 @@
   \input{pversion}
 *}
 
-
-
 end