src/HOL/MicroJava/J/Term.thy
changeset 58263 6c907aad90ba
parent 58249 180f1b3508ed
child 58310 91ea607a34d8
--- a/src/HOL/MicroJava/J/Term.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,9 @@
   | FAss cname expr vname 
                     expr     ("{_}_.._:=_" [10,90,99,90]90) -- "field ass."
   | Call cname expr mname 
-    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
+    "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"
+
+datatype_compat expr
 
 datatype_new stmt
   = Skip                     -- "empty statement"