diff -r 3a1edaa0dc6d -r fb0fcd278ac5 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Mon Jan 14 23:08:40 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Tue Jan 15 13:46:19 2013 +0100
@@ -44,7 +44,7 @@
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
-"aval' (N n) S = num' n" |
+"aval' (N i) S = num' i" |
 "aval' (V x) S = fun S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"