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"