diff -r 6b906beec36f -r 568fdc70e565 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Wed Mar 28 11:46:14 2012 +0200
+++ b/src/HOL/Bali/Decl.thy	Wed Mar 28 12:08:08 2012 +0200
@@ -129,11 +129,12 @@
                            acc_modi_Package_le    acc_modi_le_Package
                            acc_modi_Protected_le  acc_modi_le_Protected
 
-lemma acc_modi_Package_le_cases 
- [consumes 1,case_names Package Protected Public]:
- "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow> 
-   (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
-by (auto dest: acc_modi_Package_le)
+lemma acc_modi_Package_le_cases:
+  assumes "Package \<le> m"
+  obtains (Package) "m = Package"
+    | (Protected) "m = Protected"
+    | (Public) "m = Public"
+using assms by (auto dest: acc_modi_Package_le)
 
 
 subsubsection {* Static Modifier *}