diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -75,13 +75,13 @@
 defs
 
   foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def "BaseC == (Base, (Some Object, 
+  BaseC_def "BaseC == (Base, (Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
   foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
 				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
-  ExtC_def  "ExtC  == (Ext,  (Some Base  , 
+  ExtC_def  "ExtC  == (Ext,  (Base  , 
 			     [(vee, PrimT Integer)], 
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"