diff -r 8d40ddaa427f -r e60c7d0bb4b1 src/HOL/Library/Multiset.thy
--- 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]]