diff -r 79136ce06bdb -r 58d147683393 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Bali/WellForm.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -236,7 +236,7 @@
           under  (\<lambda> new old. accmodi old \<noteq> Private)
           entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
                              is_static new = is_static old)) \<and> 
-        (o2s \<circ> table_of (imethods i) 
+        (Option.set \<circ> table_of (imethods i) 
                hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
 	       entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
 
@@ -248,7 +248,7 @@
 
 lemma wf_idecl_hidings: 
 "wf_idecl G (I, i) \<Longrightarrow> 
-  (\<lambda>s. o2s (table_of (imethods i) s)) 
+  (\<lambda>s. Option.set (table_of (imethods i) s)) 
   hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
   entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
 apply (unfold wf_idecl_def o_def)
@@ -751,7 +751,7 @@
     show "\<not>is_static im \<and> accmodi im = Public" 
     proof -
       let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
-      let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
+      let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
       from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
 	by (simp add: imethds_rec)
       from wf if_I have 
@@ -1783,7 +1783,7 @@
       by (blast dest: subint1D)
 
     let ?newMethods 
-          = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
+          = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
     show "?Concl I"
     proof (cases "?newMethods sig = {}")
       case True
@@ -1864,7 +1864,7 @@
 apply (drule (1) wf_prog_idecl)
 apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
                                        [THEN is_acc_ifaceD [THEN conjunct1]]]])
-apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
+apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
                   sig ={}")
 apply   force