# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1473665365 -7200
# Node ID 32690ddf614fe5fee8d878e97bea6e6ce8b86920
# Parent  0dd6731060d72297d21f0e1d0f7d94a170dee024
more robust multiset simproc

diff -r 0dd6731060d7 -r 32690ddf614f src/HOL/Library/multiset_simprocs_util.ML
--- a/src/HOL/Library/multiset_simprocs_util.ML	Mon Sep 12 08:23:59 2016 +0200
+++ b/src/HOL/Library/multiset_simprocs_util.ML	Mon Sep 12 09:29:25 2016 +0200
@@ -27,11 +27,16 @@
 
 (*** Utilities ***)
 
+(*repeat_mset is not symmetric, unlike multiplication over natural numbers.*)
 fun mk_repeat_mset (t, u) =
   let
     val T = fastype_of t;
     val U = fastype_of u;
-  in Const (@{const_name "repeat_mset"}, T --> U --> U) $ t $ u end;
+  in
+    if T = @{typ nat}
+    then Const (@{const_name "repeat_mset"}, T --> U --> U) $ t $ u
+    else Const (@{const_name "repeat_mset"}, U --> T --> T) $ u $ t
+  end;
 
 (*Maps n to #n for n = 1, 2*)
 val numeral_syms = [@{thm numeral_One} RS sym, @{thm numeral_2_eq_2} RS sym,