diff -r d3d4ec6c21ef -r 22bc39064290 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Mar 25 10:41:53 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 25 10:44:57 2015 +0100
@@ -1658,7 +1658,7 @@
  apply (simp (no_asm))
  apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  apply (simp (no_asm_simp) add: add.assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
  apply (simp add: diff_union_single_conv)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
@@ -1669,7 +1669,7 @@
  apply (rule conjI)
   apply (simp add: multiset_eq_iff split: nat_diff_split)
  apply (rule conjI)
-  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
+  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
   apply (simp add: multiset_eq_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
@@ -1692,7 +1692,7 @@
  apply (simp add: mult1_def set_of_def, blast)
 txt {* Now we know @{term "J' \<noteq> {#}"}. *}
 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp)
 apply (erule ssubst)
 apply (simp add: Ball_def, auto)
 apply (subgoal_tac