diff -r 79136ce06bdb -r 58d147683393 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Bali/Example.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -458,7 +458,7 @@
 lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
 
 lemma imethds_HasFoo [simp]: 
-  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
+  "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
 apply (rule trans)
 apply (rule imethds_rec')
 apply  (auto simp add: HasFooInt_def)