diff -r 35c570891a3a -r 98236fbd8aa6 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Dec 03 13:51:07 2010 +0000
@@ -255,7 +255,7 @@
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   apply(rule_tac [!] equivpI)
-  unfolding reflp_def symp_def transp_def
+  unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition