diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/JVM/Store.thy
--- a/src/HOL/MicroJava/JVM/Store.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Store.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -12,9 +12,9 @@
 Store = Conform +  
 
 syntax
- value	:: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b"			("_ \\<And> _")		
+ map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b"	("_ !! _")
 translations
- "t \\<And> x"  == "the (t x)"
+ "t !! x"  == "the (t x)"
 
 constdefs
  newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"