--- a/src/HOL/Library/Multiset.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Oct 06 15:14:28 2015 +0200
@@ -2544,7 +2544,7 @@
using rel_mset_imp_rel_mset' rel_mset'_imp_rel_mset by auto
text \<open>The main end product for @{const rel_mset}: inductive characterization:\<close>
-theorems rel_mset_induct[case_names empty add, induct pred: rel_mset] =
+lemmas rel_mset_induct[case_names empty add, induct pred: rel_mset] =
rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]