diff -r 5e5ca36692b3 -r 9caab698dbe4 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Apr 03 16:26:48 2012 +0200
@@ -1111,14 +1111,12 @@
 
 text {* Operations on alists with distinct keys *}
 
-quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
-where
-  "join" is "join_raw :: ('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
+lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
+is join_raw
 by (simp add: distinct_join_raw)
 
-quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
-where
-  "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" 
+lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
+is subtract_entries_raw 
 by (simp add: distinct_subtract_entries_raw)
 
 text {* Implementing multisets by means of association lists *}