HOL-IMP: respect set/pred distinction

--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:02:17 2011 -0700
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 17 15:03:30 2011 -0700
@@ -132,7 +132,7 @@
                simp: hoare_valid_def)
 
 lemma equiv_up_to_if:
-  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
    P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
   by (auto simp: bequiv_up_to_def equiv_up_to_def)
 
@@ -162,4 +162,4 @@
   by (blast dest: while_never)
 
 
-end
\ No newline at end of file
+end