
diff -r 99c80c2f841a -r 9ace9e5b79be src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jan 17 09:38:30 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 10:45:42 2012 +0100
@@ -1078,7 +1078,7 @@
 qed auto
 
 definition
-  "subtract_entries_raw xs ys = foldr (%(k, v). AList_Impl.map_entry k (%v'. v' - v)) ys xs"
+  "subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
 
 lemma map_of_subtract_entries_raw:
   "distinct (map fst ys) ==> map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => (case map_of ys x of None => Some v | Some v' => Some (v - v')))"




