diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/Example.thy	Sun Feb 16 18:39:40 2014 +0100
@@ -458,7 +458,7 @@
 lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
 
 lemma imethds_HasFoo [simp]: 
-  "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
+  "imethds tprg HasFoo = set_option \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
 apply (rule trans)
 apply (rule imethds_rec')
 apply  (auto simp add: HasFooInt_def)