diff -r 5e5ca36692b3 -r 9caab698dbe4 src/HOL/Quotient_Examples/Lift_Set.thy
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Tue Apr 03 16:26:48 2012 +0200
@@ -2,7 +2,7 @@
     Author:     Lukas Bulwahn and Ondrej Kuncar
 *)
 
-header {* Example of lifting definitions with the quotient infrastructure *}
+header {* Example of lifting definitions with the lifting infrastructure *}
 
 theory Lift_Set
 imports Main
@@ -16,19 +16,14 @@
 
 setup_lifting type_definition_set[unfolded set_def]
 
-text {* Now, we can employ quotient_definition to lift definitions. *}
+text {* Now, we can employ lift_definition to lift definitions. *}
 
-quotient_definition empty where "empty :: 'a set"
-is "bot :: 'a \<Rightarrow> bool" done
+lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
 
 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 insertp done
+lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
 
 term "Lift_Set.insert"
 thm Lift_Set.insert_def