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