diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/AxSem.thy
--- 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}"