--- a/src/HOL/Bali/DeclConcepts.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sun Feb 16 18:39:40 2014 +0100
@@ -1402,7 +1402,7 @@
imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I =
iface_rec G I (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
- (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
+ (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
definition
@@ -1543,7 +1543,7 @@
lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set (isuperIfs i)) \<oplus>\<oplus>
- (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
+ (set_option \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
apply (unfold imethds_def)
apply (rule iface_rec [THEN trans])
apply auto