--- a/Nominal/Ex/Classical.thy	Thu Jun 23 22:21:43 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Fri Jun 24 10:12:47 2011 +0900
@@ -46,6 +46,9 @@
 thm trm.supp
 thm trm.supp[simplified]
 
+lemma swap_at_base_sort: "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x"
+  by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1))
+
 nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *)
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
@@ -74,45 +77,20 @@
   -- "covered all cases"
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
-  apply(simp)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)  
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(blast)  
-  apply(simp add: fresh_star_def)
-  apply(blast)
-  apply(simp add: fresh_star_def)
-  apply(metis)
-  apply(simp add: fresh_star_def)
-  apply(metis)  
-  apply(simp add: fresh_star_def)
-  apply(metis)
+  apply (simp_all add: fresh_star_def)[12]
+  apply(metis)+
   -- "compatibility"
   apply(simp_all)
   apply(rule conjI)
-  apply(erule conjE)+
+  apply(elim conjE)
   apply(erule Abs_lst1_fcb)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: Abs_fresh_iff)
   apply(erule fresh_eqvt_at)
   apply(simp add: finite_supp)
   apply(simp add: fresh_Pair fresh_at_base(1))
-  apply(drule sym)
-  apply(drule sym)
-  apply(drule sym)
-  apply(drule sym)
-  apply(simp add: eqvt_at_def swap_fresh_fresh)
+  apply(simp add: eqvt_at_def swap_at_base_sort)
+  apply simp
   oops
 
 end