--- a/Nominal/Ex/Foo2.thy	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Tue Dec 14 14:23:40 2010 +0000
@@ -24,12 +24,6 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
-thm foo.exhaust
-
-ML {* 
-  Variable.import;
-  Variable.import true @{thms foo.exhaust} @{context}
-*}
 
 thm foo.bn_defs
 thm foo.permute_bn
@@ -53,6 +47,26 @@
 thm foo.supp
 thm foo.fresh
 
+(*
+lemma ex_prop:
+  shows "\<exists>n::nat. Suc n = n"
+sorry
+
+lemma test:
+  shows "True"
+apply -
+ML_prf {*
+  val (x, ctxt') = Obtain.result (K (
+  EVERY [print_tac "test", 
+         etac exE 1,
+         print_tac "end"])) 
+  @{thms ex_prop} @{context};
+  ProofContext.verbose := true;
+  ProofContext.pretty_context ctxt'
+  |> Pretty.block
+  |> Pretty.writeln
+*}
+*)
 
 
 text {* *}
@@ -103,7 +117,7 @@
   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in foo.exhaust(1))
+apply(rule_tac foo.exhaust(1))
 apply(rule assms(1))
 apply(rule exI)+
 apply(assumption)
@@ -111,14 +125,7 @@
 apply(rule exI)+
 apply(assumption)
 (* lam case *)
-(*
-apply(rule Let1_rename)
-apply(rule assms(3))
-apply(assumption)
-apply(simp)
-*)
-
-apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
+apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
 apply(erule exE)
 apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
@@ -126,7 +133,7 @@
 apply(drule_tac x="trm" in meta_spec)
 apply(simp only: fresh_star_Pair set.simps)
 apply(drule meta_mp)
-apply(simp)
+apply(simp add: fresh_star_def fresh_Nil fresh_Cons fresh_atom_at_base)
 apply(erule exE)
 apply(rule assms(3))
 apply(perm_simp)