# HG changeset patch
# User nipkow
# Date 1367317601 -7200
# Node ID 8deb369ee70b4b0bfed728f0ef453703e9eb1b1b
# Parent  3be0a5c6dc9e9db6a2103cb9c4db6618d550eadf
tuned

diff -r 3be0a5c6dc9e -r 8deb369ee70b src/HOL/IMP/Abs_Int2.thy
--- 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)