diff -r c25386402f6a -r 4cf3a4d36799 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Sat May 12 20:54:00 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue May 22 14:00:59 2012 +0200
@@ -457,10 +457,22 @@
 
 section {* Quotient types *}
 
-quotient_type 
+(* FIXME: The three could be defined together, but due to bugs
+   introduced by the lifting package it doesn't work anymore *)
+quotient_type
     'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
-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 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_type
+    'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
+  apply(rule_tac [!] equivpI)
+  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_type
+   'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   apply(rule_tac [!] equivpI)
   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:)