src/HOL/Bali/WellForm.thy
changeset 28524 644b62cf678f
parent 24019 67bde7cfcf10
child 30235 58d147683393
--- a/src/HOL/Bali/WellForm.thy	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Bali/WellForm.thy	Tue Oct 07 16:07:50 2008 +0200
@@ -562,7 +562,7 @@
 lemma class_Object [simp]: 
 "wf_prog G \<Longrightarrow> 
   class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
-                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>"
+                                  init=Skip,super=undefined,superIfs=[]\<rparr>"
 apply (unfold wf_prog_def Let_def ObjectC_def)
 apply (fast dest!: map_of_SomeI)
 done