src/HOL/Bali/DeclConcepts.thy
changeset 55518 1ddb2edf5ceb
parent 46714 a7ca72710dfe
child 58887 38db8ddc0f57
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sun Feb 16 17:50:13 2014 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sun Feb 16 18:39:40 2014 +0100
     1.3 @@ -1402,7 +1402,7 @@
     1.4    imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
     1.5    "imethds G I =
     1.6      iface_rec G I  (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
     1.7 -                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     1.8 +                        (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     1.9  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    1.10  
    1.11  definition
    1.12 @@ -1543,7 +1543,7 @@
    1.13  
    1.14  lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
    1.15    imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
    1.16 -                      (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    1.17 +                      (set_option \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    1.18  apply (unfold imethds_def)
    1.19  apply (rule iface_rec [THEN trans])
    1.20  apply auto