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