src/HOL/Library/multiset_order_simprocs.ML

--- a/src/HOL/Library/multiset_order_simprocs.ML	Mon Feb 13 16:03:55 2017 +0100
+++ b/src/HOL/Library/multiset_order_simprocs.ML	Tue Feb 14 18:32:53 2017 +0100
@@ -13,20 +13,20 @@
 structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS =
 struct
 
-structure LessCancelMultiset = CancelNumeralsFun
- (open Multiset_Cancel_Common
+structure LessCancelMultiset = Cancel_Fun
+ (open Cancel_Data
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
-  val bal_add1 = @{thm mset_less_add_iff1} RS trans
-  val bal_add2 = @{thm mset_less_add_iff2} RS trans
+  val bal_add1 = @{thm mset_less_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
+  val bal_add2 = @{thm mset_less_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
 );
 
-structure LeCancelMultiset = CancelNumeralsFun
- (open Multiset_Cancel_Common
+structure LeCancelMultiset = Cancel_Fun
+ (open Cancel_Data
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
-  val bal_add1 = @{thm mset_le_add_iff1} RS trans
-  val bal_add2 = @{thm mset_le_add_iff2} RS trans
+  val bal_add1 = @{thm mset_le_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
+  val bal_add2 = @{thm mset_le_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
 );
 
 val less_cancel_msets = LessCancelMultiset.proc;