--- 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 *)