# HG changeset patch
# User kleing
# Date 1376122530 -7200
# Node ID 07423b37bc225ab60faf32c51e9eb786b0130a01
# Parent  de4bccddcdbdfdef09d2a43495d64d684f13571d
avoid unnecessary case distinction

diff -r de4bccddcdbd -r 07423b37bc22 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Sat Aug 10 09:06:42 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Sat Aug 10 10:15:30 2013 +0200
@@ -107,7 +107,7 @@
   "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
    P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
   unfolding exec1_def
-  by (auto split: instr.split)
+  by (auto simp del: iexec.simps)
 
 lemma exec_appendL:
   fixes i i' :: int