src/HOL/NanoJava/OpSem.thy

--- a/src/HOL/NanoJava/OpSem.thy	Sun Oct 14 22:15:07 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Mon Oct 15 17:02:57 2001 +0200
@@ -54,7 +54,7 @@
             s -Cast C e>v-n-> s'"
 
   Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
-            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s2)) -Meth (C,m)-n-> s3
+            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3
      |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
 
   Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;