# HG changeset patch
# User nipkow
# Date 1367380855 -7200
# Node ID 19ee0cebe76d75a7175e32d6345bf5a457787b0a
# Parent  ed847ce0b70cf7d6a2a49e7767e28fa22ed75a05
tuned

diff -r ed847ce0b70c -r 19ee0cebe76d src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed May 01 03:56:57 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed May 01 06:00:55 2013 +0200
@@ -111,8 +111,8 @@
   obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>s S'" using `s : \<gamma>\<^isub>o S`
     by(auto simp: in_gamma_option_iff)
   moreover hence "s x : \<gamma> (fun S' x)"
-    using V(1,2) by(simp add: \<gamma>_st_def)
-  moreover have "s x : \<gamma> a" using V by simp
+    by(simp add: \<gamma>_st_def)
+  moreover have "s x : \<gamma> a" using V(2) by simp
   ultimately show ?case
     by(simp add: Let_def \<gamma>_st_def)
       (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)