--- a/src/HOL/Bali/Trans.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Bali/Trans.thy Tue Oct 07 16:07:50 2008 +0200
@@ -81,7 +81,7 @@
\<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
\<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk>
\<Longrightarrow>
- G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
+ G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
\<Longrightarrow>