diff -r 3d28e437581b -r 649680775e93 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 11 15:08:45 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 16:05:15 2010 +0100
@@ -1190,12 +1190,18 @@
   apply (rule refl)
 done
 
+
+
+
+
+atom_decl name2
+
 datatype rfoo8 =
   Foo0 "name"
 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
 and rbar8 =
-  Bar0 "name"
-| Bar1 "name" "name" "rbar8" --"bind second name in b"
+  Bar0 "name2"
+| Bar1 "name" "name2" "rbar8" --"bind second name in b"
 
 primrec
   rbv8
@@ -1242,21 +1248,24 @@
   apply (erule alpha8f_alpha8b.inducts(2))
   apply (simp_all)
 done
-
 lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"
   apply simp apply clarify
   apply (erule alpha8f_alpha8b.inducts(2))
-  apply (simp_all add:alpha_gen)
+  apply (simp_all add: alpha_gen)
 done
 
-lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"
-  apply simp apply clarify
-  apply (erule alpha8f_alpha8b.inducts(1))
-  apply (simp_all add:alpha_gen)
-  apply (clarify)
-sorry (* ??? *)
-
-
+lemma "(c :: name2) \<noteq> b \<Longrightarrow> (atom (a :: name)) \<noteq> (atom b) \<Longrightarrow> \<not> (alpha8f ===> op =) rfv_foo8 rfv_foo8"
+  apply (simp_all)
+  apply (rule_tac x="Foo1 (Bar1 a c (Bar0 c)) (Foo0 a)" in exI)
+  apply (rule_tac x="Foo1 (Bar1 a c (Bar0 b)) (Foo0 a)" in exI)
+  apply (rule conjI)
+  apply (rule a3)
+  apply (rule_tac x="0 :: perm" in exI)
+  apply (simp add: alpha_gen fresh_star_def)
+  apply (rule a1)
+  apply (rule refl)
+  apply simp
+done