diff -r 4bee6d8c1500 -r 7c507e664047 src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Nov 10 10:29:19 2014 +0100
@@ -39,21 +39,21 @@
 
 subsection {* Lifted constant definitions *}
 
-lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer .
+lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric list.ctr_transfer(1) .
 
-lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
+lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric list.ctr_transfer(2)
   by simp
 
 lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append parametric append_transfer
   by simp
 
-lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric map_transfer
+lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric list.map_transfer
   by simp
 
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter parametric filter_transfer
   by simp
 
-lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric set_transfer
+lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric list.set_transfer
   by simp
 
 text {* Constants with nested types (like concat) yield a more