--- a/Nominal/ExLet.thy	Fri Apr 02 03:23:25 2010 +0200
+++ b/Nominal/ExLet.thy	Fri Apr 02 05:09:47 2010 +0200
@@ -123,6 +123,8 @@
   apply(simp_all add:permute_bn eqvts)
   done
 
+thm trm_lts.inducts[no_vars]
+
 lemma 
   fixes t::trm
   and   l::lts