src/HOL/MicroJava/J/Term.thy
changeset 10763 08e1610c1dcb
parent 10119 20c9590bb5f5
child 11026 a50365d21144
--- a/src/HOL/MicroJava/J/Term.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -20,8 +20,9 @@
   | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
   | FAss cname expr vname 
                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
-  | Call expr mname 
-    (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
+  | Call cname expr mname 
+    (ty list) (expr list)    (* method call*) ("{_}_.._'( {_}_')"
+                                                            [10,90,99,10,10] 90)
 
 datatype stmt
   = Skip                     (* empty statement *)