--- a/Quot/Examples/LFex.thy	Mon Dec 21 23:13:40 2009 +0100
+++ b/Quot/Examples/LFex.thy	Tue Dec 22 07:28:09 2009 +0100
@@ -277,6 +277,7 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8
 *)
 
+
 lemma "\<lbrakk>P TYP;
   \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);
   \<And>id. Q (TCONST id);