--- a/Paper/Paper.thy	Mon Feb 21 03:33:27 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 21 03:35:39 2011 +0000
@@ -1161,7 +1161,7 @@
   
   \noindent
   The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
-  we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the 
+  we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 
   empty string, we 
   have the following picture:
   %