diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Quotient_Examples/Lift_Set.thy
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -8,9 +8,9 @@
 imports Main
 begin
 
-definition set where "set = (UNIV :: ('a => bool) => bool)"
+definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
 
-typedef (open) 'a set = "set :: 'a set set"
+typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
   morphisms member Set
   unfolding set_def by auto
 
@@ -37,15 +37,19 @@
 text {* Now, we can employ quotient_definition to lift definitions. *}
 
 quotient_definition empty where "empty :: 'a set"
-is "Set.empty"
+is "bot :: 'a \<Rightarrow> bool"
 
 term "Lift_Set.empty"
 thm Lift_Set.empty_def
 
+definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
+  "insertp x P y \<longleftrightarrow> y = x \<or> P y"
+
 quotient_definition insert where "insert :: 'a => 'a set => 'a set"
-is "Set.insert"
+is insertp
 
 term "Lift_Set.insert"
 thm Lift_Set.insert_def
 
 end
+