diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/JVM/Object.thy
--- a/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 16:32:51 2000 +0200
@@ -65,7 +65,7 @@
 primrec
   "exec_ch (Checkcast C) G hp stk pc =
 	(let oref	= hd stk;
-	     xp'	= raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
+	     xp'	= raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast;
 	     stk'	= if xp'=None then stk else tl stk
 	 in
 	 (xp' , stk' , pc+1))"