diff -r 85b13d75b2e4 -r 6c907aad90ba src/HOL/MicroJava/J/Term.thy
--- 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"