--- a/Nominal/Test.thy	Tue Mar 16 18:02:08 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 18:13:34 2010 +0100
@@ -43,8 +43,8 @@
   by (rule eqvts)
 
 lemma supp_fv:
-  "supp t = fv_lam t" and 
-  "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
+  shows "supp t = fv_lam t" 
+  and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
 apply(induct t and bp rule: lam_bp_inducts)
 apply(simp_all add: lam_bp_fv)
 (* VAR case *)
@@ -107,6 +107,8 @@
 apply(blast)
 done
 
+thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+
 text {* example 2 *}
 
 nominal_datatype trm' =