src/HOL/MicroJava/J/Example.ML

--- a/src/HOL/MicroJava/J/Example.ML	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.ML	Tue Jan 02 22:41:17 2001 +0100
@@ -195,7 +195,7 @@
 
 fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
 Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
-\ Expr(e::=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
+\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
 (* ?pTs' = [Class Base] *)
 by t;		(* ;; *)
 by  t;		(* Expr *)