
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -48,7 +48,7 @@
 
 lemma [quot_respect]:
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
   apply (rule TrueI)+




