src/HOL/MicroJava/J/WellForm.thy

 	(\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and>  unique ms \\<and>
 	(case sc of None \\<Rightarrow> C = Object
          | Some D \\<Rightarrow>
              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<prec>C C \\<and>
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
-                 cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+                 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
 
  wf_prog	:: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
 "wf_prog wtm G \\<equiv>
    let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"