diff -r 409ecb7284dd -r 5686d83db1f9 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Wed May 12 14:47:52 2010 +0100
@@ -16,7 +16,7 @@
 where
   "bn (As x t) = {atom x}"
 
-
+ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff
@@ -31,6 +31,7 @@
 equivariance alpha_trm_raw
 
 
+
 end