src/HOL/Bali/WellType.thy
changeset 30235 58d147683393
parent 27239 f2f42f9fa09d
child 32960 69916a850301
--- a/src/HOL/Bali/WellType.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Bali/WellType.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -87,11 +87,11 @@
 defs
  cmheads_def:
 "cmheads G S C 
-  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
+  \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
   Objectmheads_def:
 "Objectmheads G S  
   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
-    ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
+    ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
   accObjectmheads_def:
 "accObjectmheads G S T
    \<equiv> if G\<turnstile>RefT T accessible_in (pid S)