src/HOL/IMP/Vars.thy

--- a/src/HOL/IMP/Vars.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Vars.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -41,7 +41,7 @@
 begin
 
 fun vars_bexp :: "bexp \<Rightarrow> name set" where
-"vars_bexp (B bv) = {}" |
+"vars_bexp (Bc v) = {}" |
 "vars_bexp (Not b) = vars_bexp b" |
 "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
 "vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"