--- a/Paper/Paper.thy	Thu Apr 01 14:09:47 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 14:50:58 2010 +0200
@@ -1692,9 +1692,9 @@
 %%  @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
 %%  @{text "\<dots>"}\\
   @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\
-  @{text "\<^raw:\hspace{2cm}>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
+  @{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
   @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\
-  @{text "\<^raw:\hspace{2cm}>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
+  @{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
   @{text "\<dots>"}
   \end{tabular}
 }