diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -42,8 +42,8 @@
 
   (* cf. 15.15 *)
   Cast	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
-	  x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
-			        G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)"
+	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
+			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v\\<rightarrow> (x2,s1)"
 
   (* cf. 15.7.1 *)
   Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"