--- a/src/HOL/MicroJava/JVM/Method.thy Mon Nov 29 11:21:50 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy Mon Nov 29 14:12:53 1999 +0100
@@ -23,7 +23,7 @@
argsoref = take (n+1) stk;
oref = last argsoref;
xp' = raise_xcpt (oref=Null) NullPointer;
- dynT = fst(hp !! (the_Addr oref));
+ dynT = fst(the(hp(the_Addr oref)));
(dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
frs' = if xp'=None
then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
--- a/src/HOL/MicroJava/JVM/Object.thy Mon Nov 29 11:21:50 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Object.thy Mon Nov 29 14:12:53 1999 +0100
@@ -39,8 +39,8 @@
"exec_mo (Getfield F C) hp stk pc =
(let oref = hd stk;
xp' = raise_xcpt (oref=Null) NullPointer;
- (oc,fs) = hp !! (the_Addr oref);
- stk' = if xp'=None then (fs!!(F,C))#(tl stk) else tl stk
+ (oc,fs) = the(hp(the_Addr oref));
+ stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk
in
(xp' , hp , stk' , pc+1))"
@@ -48,7 +48,7 @@
(let (fval,oref)= (hd stk, hd(tl stk));
xp' = raise_xcpt (oref=Null) NullPointer;
a = the_Addr oref;
- (oc,fs) = hp !! a;
+ (oc,fs) = the(hp a);
hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
in
(xp' , hp' , tl (tl stk), pc+1))"
--- a/src/HOL/MicroJava/JVM/Store.thy Mon Nov 29 11:21:50 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Store.thy Mon Nov 29 14:12:53 1999 +0100
@@ -11,11 +11,6 @@
Store = Conform +
-syntax
- map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _")
-translations
- "t !! x" == "the (t x)"
-
constdefs
newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
"newref s \\<equiv> \\<epsilon>v. s v = None"