diff -r 1c77e15c4259 -r f0252365936c Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Nov 15 09:52:29 2010 +0000
@@ -7,6 +7,7 @@
   binding function
 *}
 
+
 atom_decl name
 
 nominal_datatype foo: trm =
@@ -49,6 +50,7 @@
 thm foo.fsupp
 thm foo.supp
 thm foo.fresh
+thm foo.bn_finite
 
 lemma uu1:
   shows "alpha_bn1 as (permute_bn1 p as)"
@@ -124,13 +126,6 @@
 apply(simp add: atom_eqvt insert_eqvt)
 done
 
-lemma bn_finite:
-  shows "(\<lambda>x. True) t"
-  and  "finite (set (bn1 as)) \<and> finite (set (bn2 as)) \<and> finite (set (bn3 as))"
-  and  "finite (bn4 as')"
-apply(induct "t::trm" and as and as' rule: foo.inducts)
-apply(simp_all add: foo.bn_defs)
-done
 
 
 lemma strong_exhaust1:
@@ -154,6 +149,7 @@
 apply(rule assms(3))
 apply(perm_simp)
 apply(assumption)
+apply(simp)
 apply(drule supp_perm_eq[symmetric])
 apply(perm_simp)
 apply(simp)
@@ -216,12 +212,13 @@
 apply(simp)
 apply(simp add: tt4 uu4)
 apply(rule at_set_avoiding2)
-apply(simp add: bn_finite)
+apply(simp add: foo.bn_finite)
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: Abs_fresh_star)
 done
 
+
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
   shows "P"