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 *)