diff -r fe25a3ffeb14 -r b1b648933850 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 14:37:59 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 23:34:30 2010 +0200
@@ -58,34 +58,49 @@
   "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
-apply(auto)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule refl)
+apply(assumption)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(assumption)
 apply(assumption)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
-apply(simp add: a1)
+apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(rule refl)
+apply(assumption)
 done
 
 lemma [quot_respect]: