src/HOL/Transcendental.thy

--- a/src/HOL/Transcendental.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Transcendental.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -36,7 +36,7 @@
 apply (subst setsum_op_ivl_Suc)
 apply (subst lemma_realpow_diff_sumr)
 apply (simp add: right_distrib del: setsum_op_ivl_Suc)
-apply (subst mult_left_commute [where a="x - y"])
+apply (subst mult_left_commute [of "x - y"])
 apply (erule subst)
 apply (simp add: algebra_simps)
 done