--- a/src/HOL/Bali/AxSem.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Bali/AxSem.thy Tue Oct 07 16:07:50 2008 +0200
@@ -501,7 +501,7 @@
| hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
-| Abrupt: "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
+| Abrupt: "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
--{* variables *}
| LVar: " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"