--- a/Quot/Examples/LFex.thy	Mon Dec 07 15:18:44 2009 +0100
+++ b/Quot/Examples/LFex.thy	Mon Dec 07 15:21:51 2009 +0100
@@ -180,6 +180,8 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
+end
+
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
 lemma kpi_rsp[quotient_rsp]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
@@ -299,9 +301,8 @@
 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 done
 
-print_quotients
-
 end
 
 
 
+