--- a/Nominal/Ex/Let.thy	Sat Feb 05 07:39:00 2011 +0900
+++ b/Nominal/Ex/Let.thy	Mon Feb 07 15:59:37 2011 +0000
@@ -100,6 +100,7 @@
 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"
 | "substa s t ANil = ANil"
 | "substa s t (ACons v t' as) = ACons v (subst v t t') as"
+oops
 
 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r")
 defer
@@ -113,6 +114,7 @@
 apply rule
 apply (rule subst_substa_graph.intros)*)
 
+(*
 defer
 apply (case_tac x)
 apply (case_tac a)
@@ -163,7 +165,7 @@
          (Acons s (subst a t t') a2)
 
 ACons v (subst v t t') as"
-
+*)
 end