diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/JVM/Object.thy
--- a/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 20:47:11 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 (ClassT C) hp oref) ClassCast;
+	     xp'	= raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
 	     stk'	= if xp'=None then stk else tl stk
 	 in
 	 (xp' , stk' , pc+1))"