diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -77,6 +77,7 @@
   apply(metis)+
   -- "compatibility"
   apply(all_trivials)
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(rule conjI)
   apply(elim conjE)
@@ -280,6 +281,7 @@
   apply (simp_all add: fresh_star_def)[12]
   apply(metis)+
   -- "compatibility"
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(rule conjI)
   apply(elim conjE)
@@ -479,18 +481,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)
   apply (simp_all add: fresh_star_def fresh_Pair)[12]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(rule obtain_fresh)
-  apply(auto)[1]
-  apply(metis)+
-  -- "compatibility"
-  apply(all_trivials)
-  apply(simp)
+  apply(metis)
   oops
 
 end