# HG changeset patch
# User nipkow
# Date 943881173 -3600
# Node ID a13c3b80d3d47a7524d4cf504ae2af55a5424772
# Parent  18f10850aca5c4be19a0579c089cd1301f91ee92
Removed !!

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