# HG changeset patch
# User nipkow
# Date 1323253485 -3600
# Node ID 9b11989f38b0d68de19a24acba69018659a7a7d5
# Parent  7f2366dc8c0f83d61217c1b4581f0c664c6ea01c
tuned

diff -r 7f2366dc8c0f -r 9b11989f38b0 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Tue Dec 06 15:23:16 2011 +0100
+++ b/src/HOL/IMP/Vars.thy	Wed Dec 07 11:24:45 2011 +0100
@@ -42,9 +42,9 @@
 begin
 
 fun vars_aexp :: "aexp \<Rightarrow> vname set" where
-"vars_aexp (N n) = {}" |
-"vars_aexp (V x) = {x}" |
-"vars_aexp (Plus a\<^isub>1 a\<^isub>2) = vars_aexp a\<^isub>1 \<union> vars_aexp a\<^isub>2"
+"vars (N n) = {}" |
+"vars (V x) = {x}" |
+"vars (Plus a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
 
 instance ..
 
@@ -60,10 +60,10 @@
 begin
 
 fun vars_bexp :: "bexp \<Rightarrow> vname set" where
-"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"
+"vars (Bc v) = {}" |
+"vars (Not b) = vars b" |
+"vars (And b\<^isub>1 b\<^isub>2) = vars b\<^isub>1 \<union> vars b\<^isub>2" |
+"vars (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"
 
 instance ..