--- a/Nominal/Ex/ExLet.thy	Sat Apr 03 22:31:11 2010 +0200
+++ b/Nominal/Ex/ExLet.thy	Sun Apr 04 21:39:28 2010 +0200
@@ -167,6 +167,7 @@
     apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
     apply(erule exE)
     apply(erule conjE)
+    thm Lt_subst
     apply(subst Lt_subst)
     apply assumption
     apply(rule a4)