--- a/Pearl/Paper.thy	Thu Apr 08 00:01:45 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 00:09:53 2010 -0700
@@ -890,10 +890,10 @@
 
   The following Isabelle/HOL command defines a concrete atom type called
   \emph{name}, which consists of atoms whose sort equals the string @{term
-  "''name''"}.
+  "''Thy.name''"}.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"}
   \end{isabelle}
 
   \noindent