diff -r 11402be6e4b0 -r 06c1998340a8 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Tue Aug 07 22:42:22 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Wed Aug 08 12:36:48 2001 +0200
@@ -23,20 +23,22 @@
 
 datatype stmt
   = Skip                   (* empty statement *)
-  | Comp       stmt stmt   ("_;; _"             [91,90]    90)
-  | Cond vname stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
+  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
+  | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
-
-  | NewC vname cname       ("_:=new _"  [99,   99] 95) (* object creation  *)
-  | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
-  | FAcc vname vname vnam  ("_:=_.._"   [99,99,99] 95) (* field access     *)
-  | FAss vname vnam  vname ("_.._:=_"   [99,99,99] 95) (* field assigment  *)
-  | Call vname cname vname mname vname                 (* method call      *)
-                           ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
+  | 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 *)
+and expr
+  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
+  | Cast cname expr                              (* type cast        *)
+  | LAcc vname                                   (* local access     *)
+  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
+  | Call cname expr mname expr                   (* method call      *)
+                     ("{_}_.._'(_')" [99,95,99,95] 95)
 
-(*###TO Product_Type_lemmas.ML*)
+
 lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
 apply (rule_tac x = "(a,b)" in image_eqI)
 apply  auto