tuned

--- a/src/HOL/IMP/Abs_Int2.thy	Tue Apr 30 12:18:40 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Apr 30 12:26:41 2013 +0200
@@ -67,7 +67,7 @@
 
 fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
 "aval'' e None = \<bottom>" |
-"aval'' e (Some sa) = aval' e sa"
+"aval'' e (Some S) = aval' e S"
 
 lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
 by(cases S)(auto simp add: aval'_sound split: option.splits)