diff -r 89ccda903f4a -r bacf3584640e Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -17,7 +17,6 @@
   | Var "name"
   | App "trm" "trm"
   | Lam "ty" "name" "trm"
-print_theorems
 
 primrec
     rfv_kind :: "kind \<Rightarrow> atom set"
@@ -33,7 +32,6 @@
 | "rfv_trm (Var x) = {atom x}"
 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
-print_theorems
 
 instantiation kind and ty and trm :: pt
 begin