diff -r ca089b9d13c4 -r d3916d9183d2 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Thu Aug 07 17:46:50 2003 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Aug 08 14:54:37 2003 +0200
@@ -193,6 +193,13 @@
 apply (fast)
 done
 
+lemma exec_no_xcpt: "G \<turnstile> (x, s) -c-> (None, s')
+\<Longrightarrow> x = None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct2 [THEN conjunct2], rule_format])
+apply simp+
+done
+
+
 lemma eval_evals_exec_xcpt: 
 "!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>  
          (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>