diff -r c0695bb33fcd -r 320775fa47ca Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:10:36 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:56:28 2010 -0400
@@ -37,7 +37,8 @@
 thm single_let.supp
 thm single_let.size
 
-
+thm single_let.supp(1-2)
+thm single_let.fv_defs[simplified single_let.supp(1-2)]
 
 
 end