1.1 --- a/src/HOL/Bali/WellType.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -87,11 +87,11 @@
     1.4  defs
     1.5   cmheads_def:
     1.6  "cmheads G S C 
     1.7 -  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
     1.8 +  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
     1.9    Objectmheads_def:
    1.10  "Objectmheads G S  
    1.11    \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    1.12 -    ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    1.13 +    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    1.14    accObjectmheads_def:
    1.15  "accObjectmheads G S T
    1.16     \<equiv> if G\<turnstile>RefT T accessible_in (pid S)