diff -r ec63c82551ae -r 9587134ec780 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Aug 09 11:26:29 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Aug 09 12:27:29 2013 +0200
@@ -63,10 +63,6 @@
   "P \<turnstile> c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
 
-(*
-declare exec1_def [simp]
-*)
-
 lemma exec1I [intro, code_pred_intro]:
   "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
   \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"