# HG changeset patch # User fleury # 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,