src/HOL/MicroJava/J/Term.thy
changeset 9348 f495dba0cb07
parent 9346 297dcbf64526
child 10042 7164dc0d24d8
--- a/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -12,7 +12,7 @@
 
 datatype expr
 	= NewC	cname		   (* class instance creation *)
-	| Cast	ref_ty expr	   (* type cast *)
+	| Cast	cname expr	   (* type cast *)
 	| Lit	val		   (* literal value, also references *)
         | BinOp binop  expr expr   (* binary operation *)
 	| LAcc vname		   (* local (incl. parameter) access *)