--- a/src/HOL/Library/Multiset.thy Tue Oct 06 12:01:07 2015 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Oct 06 17:44:32 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]]