diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy	Thu Jan 26 09:52:47 2012 +0100
@@ -152,8 +152,8 @@
 definition CS :: "com \<Rightarrow> state set acom" where
 "CS c = lfp (step UNIV) c"
 
-lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
-proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
+lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
+proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
   case 2 thus ?case by fastforce
 next
   case 3 thus ?case by(simp add: le_post)
@@ -164,7 +164,7 @@
 qed auto
 
 lemma mono_step: "mono (step S)"
-by(blast intro: monoI mono_step_aux)
+by(blast intro: monoI mono2_step)
 
 lemma strip_step: "strip(step S c) = strip c"
 by (induction c arbitrary: S) auto