diff -r 649680775e93 -r 998d6b491003 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 11 16:05:15 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 11 16:54:04 2010 +0100
@@ -1216,6 +1216,7 @@
 | "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)"
 | "rfv_bar8 (Bar0 x) = {atom x}"
 | "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"
+print_theorems
 
 instantiation
   rfoo8 and rbar8 :: pt
@@ -1240,7 +1241,7 @@
 where
   a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
-| a3: "(\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
+| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b rfv_bar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
 
 lemma "(alpha8b ===> op =) rbv8 rbv8"
@@ -1248,28 +1249,25 @@
   apply (erule alpha8f_alpha8b.inducts(2))
   apply (simp_all)
 done
-lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"
-  apply simp apply clarify
+
+lemma rfv_bar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> rfv_bar8 x = rfv_bar8 y"
   apply (erule alpha8f_alpha8b.inducts(2))
   apply (simp_all add: alpha_gen)
 done
+lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"
+  apply simp apply clarify apply (simp add: rfv_bar8_rsp_hlp)
+done
 
-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
+lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"
+  apply simp apply clarify
+  apply (erule alpha8f_alpha8b.inducts(1))
+  apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp)
 done
 
 
 
 
+
 text {* type schemes *} 
 datatype ty = 
   Var "name"