diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -94,7 +94,7 @@
             (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-> s3;
             G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
-         G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+         G\\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
 
 
 (* evaluation of expression lists *)