--- a/src/HOL/Bali/Example.thy Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Example.thy Wed Dec 21 12:02:57 2005 +0100
@@ -1018,7 +1018,7 @@
"Ball (set standard_classes) (wf_cdecl tprg)"
apply (unfold standard_classes_def Let_def
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
-apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
+apply (simp (no_asm) add: wf_cdecl_def ws_cdecls not_Some_eq)
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def
intro: da.Skip)
apply (auto simp add: Object_def Classes_def standard_classes_def