diff -r 18f10850aca5 -r a13c3b80d3d4 src/HOL/MicroJava/JVM/Object.thy
--- 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))"