diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -152,11 +152,11 @@
   "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
   by (auto simp: equiv_up_to_def)
 
-lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
+lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
  by (induct rule: big_step_induct) auto
   
 lemma equiv_up_to_while_True [intro!,simp]:
-  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
+  "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   unfolding equiv_up_to_def
   by (blast dest: while_never)