diff -r 8fbc7d38d6cf -r 7711d60a5293 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Fri Jan 04 09:34:11 2008 +0100
@@ -71,33 +71,25 @@
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
-lemma supp_beta: 
+lemma beta_preserves_fresh: 
+  fixes a::"name"
   assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
-  shows "(supp s)\<subseteq>((supp t)::name set)"
+  shows "a\<sharp>t \<Longrightarrow> a\<sharp>s"
 using a
-by (induct)
-   (auto intro!: simp add: abs_supp lam.supp subst_supp)
+apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
+apply(auto simp add: abs_fresh fresh_fact fresh_atm)
+done
 
 lemma beta_abs: 
-  assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'"
+  assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'" 
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-using a
-apply -
-apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
-apply(auto simp add: lam.distinct lam.inject)
-apply(auto simp add: alpha)
-apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
-apply(rule conjI)
-apply(rule sym)
-apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
-apply(simp)
-apply(rule pt_name3)
-apply(simp add: at_ds5[OF at_name_inst])
-apply(rule conjI)
-apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
-apply(force dest!: supp_beta simp add: fresh_def)
-apply(force intro!: eqvts)
-done
+proof -
+  have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+  with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh)
+  with a show ?thesis
+    by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
+       (auto simp add: lam.inject abs_fresh alpha)
+qed
 
 lemma beta_subst: 
   assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"