1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Mon Aug 01 19:53:30 2011 +0200
     1.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Mon Aug 01 20:21:11 2011 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4    "1 \<le> isize (acomp a)"
     1.5    by (induct a) auto
     1.6  
     1.7 -lemma exits_acomp [simp]:
     1.8 +lemma acomp_exits [simp]:
     1.9    "exits (acomp a) = {isize (acomp a)}"
    1.10    by (auto simp: exits_def acomp_size)
    1.11