--- a/Pearl/Paper.thy	Thu Apr 08 00:09:53 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 00:25:08 2010 -0700
@@ -741,7 +741,7 @@
   provided @{thm (prem 1) finite_supp_unique[no_vars]},
   @{thm (prem 2) finite_supp_unique[no_vars]}, and for
   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
   \end{lemma}
 
   \begin{proof}