--- a/src/HOL/Bali/WellForm.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/WellForm.thy Sun Feb 16 18:39:40 2014 +0100
@@ -236,7 +236,7 @@
under (\<lambda> new old. accmodi old \<noteq> Private)
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and>
is_static new = is_static old)) \<and>
- (Option.set \<circ> table_of (imethods i)
+ (set_option \<circ> table_of (imethods i)
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
@@ -248,7 +248,7 @@
lemma wf_idecl_hidings:
"wf_idecl G (I, i) \<Longrightarrow>
- (\<lambda>s. Option.set (table_of (imethods i) s))
+ (\<lambda>s. set_option (table_of (imethods i) s))
hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))
entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
apply (unfold wf_idecl_def o_def)
@@ -753,7 +753,7 @@
show "\<not>is_static im \<and> accmodi im = Public"
proof -
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
- let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
+ let ?new = "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
by (simp add: imethds_rec)
from wf if_I have
@@ -1765,7 +1765,7 @@
by (blast dest: subint1D)
let ?newMethods
- = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
+ = "(set_option \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
show ?case
proof (cases "?newMethods sig = {}")
case True
@@ -1845,7 +1845,7 @@
apply (drule (1) wf_prog_idecl)
apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1
[THEN is_acc_ifaceD [THEN conjunct1]]]])
-apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
+apply (case_tac "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
sig ={}")
apply force