# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285931399 14400
# Node ID bcd119bb854b4418c9ddf547263419b60327aead
# Parent  68ee6913fa8ddd556cc3b1cb5c45d639b7cae829
minor experiments

diff -r 68ee6913fa8d -r bcd119bb854b Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Thu Sep 30 07:43:46 2010 -0400
+++ b/Nominal/Ex/Let.thy	Fri Oct 01 07:09:59 2010 -0400
@@ -97,12 +97,15 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs, fv_bn assn) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
+apply(simp add: set_eqvt)
+apply(subst (asm) tt)
 apply(rule_tac assms(4))
-apply(simp add: set_eqvt)
-apply(simp add: tt)
+apply(simp add: fresh_star_prod)
+apply(erule conjE)
+apply(assumption)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])