diff -r d1c2bef01e2f -r 412a3ced6efd src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Tue Oct 03 18:40:25 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.ML	Tue Oct 03 18:44:19 2000 +0200
@@ -1,4 +1,3 @@
-open Example;
 
 AddIs [widen.null];
 
@@ -130,7 +129,7 @@
 qed "method_Base";
 Addsimps [method_Base];
 
-Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \
+Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \
 \ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
 br trans 1;
 br  method_rec_ 1;