src/HOL/MicroJava/J/Example.thy

--- a/src/HOL/MicroJava/J/Example.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -86,7 +86,7 @@
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
   test_def "test == Expr(e::=NewC Ext);; 
-                    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
+                    Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
 syntax