diff -r 6ea0e7c43c4f -r e564c3d2d174 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Fri Nov 29 09:48:28 2002 +0100
@@ -75,7 +75,6 @@
 apply (simp add: gl_def)
 apply (intro strip, simp)
 apply (simp add: galldefs del: set_append map_append)
-apply (auto simp: the_map_upd)
 done