diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -72,7 +72,7 @@
   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
   Call	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
 	   G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
-	   (md,rT,pns,lvars,blk,res) = the (cmethd (G,dynT) (mn,pTs));
+	   (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
 	   G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
 	   G\\<turnstile>     s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
 			    G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"