--- a/src/HOL/NanoJava/Term.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Thu Aug 09 20:48:57 2001 +0200
@@ -14,6 +14,7 @@
arities cname :: "term"
vnam :: "term"
mname :: "term"
+types imname = "cname \<times> mname"
datatype vname (* variable for special names *)
= This (* This pointer *)
@@ -29,7 +30,7 @@
| LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *)
| FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *)
| Meth cname mname (* virtual method *)
- | Impl cname mname (* method implementation *)
+ | Impl imname (* method implementation *)
and expr
= NewC cname ("new _" [ 99] 95) (* object creation *)
| Cast cname expr (* type cast *)