--- 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"