1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Thu Nov 25 12:30:57 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Fri Nov 26 08:46:59 1999 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  defs
     1.5  
     1.6    m_head_def  "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
     1.7 -		 option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
     1.8 +		 option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (method (G,C) sig)"
     1.9                                                                 
    1.10    more_spec_def	  "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
    1.11  		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
    1.12 @@ -118,7 +118,7 @@
    1.13  
    1.14    (* cf. 15.10.1 *)
    1.15    FAcc	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C; 
    1.16 -	  cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
    1.17 +	  field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
    1.18  						 E\\<turnstile>{fd}a..fn\\<Colon>fT"
    1.19  
    1.20    (* cf. 15.25, 15.25.1 *)