diff -r 78a82c37b4b2 -r 484559628038 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jun 19 15:55:22 2015 +0200
@@ -17,7 +17,7 @@
   "tokens [] = 0"
 | "tokens (x#xs) = x + tokens xs"
 
-abbreviation (input) "bag_of \<equiv> multiset_of"
+abbreviation (input) "bag_of \<equiv> mset"
 
 lemma setsum_fun_mono [rule_format]:
      "!!f :: nat=>nat.