diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -80,8 +80,8 @@
   BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext)
-					(LAcc x)..vee:=Lit (Intg #1)),
+  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
+				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
   ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
 			     [(vee, PrimT Integer)], 
@@ -113,5 +113,5 @@
   "s0" == " Norm    (empty          ,empty                        )"
   "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a)             )"
   "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
-  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
+  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
 end