diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Jan 03 14:07:08 2000 +0100
@@ -16,7 +16,7 @@
 
 WellForm = TypeRel +
 
-types 'c wtm = 'c prog => cname => 'c mdecl => bool
+types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
 
 constdefs
 
@@ -26,22 +26,22 @@
  wf_mhead	:: "'c prog \\<Rightarrow> sig   \\<Rightarrow> ty \\<Rightarrow> bool"
 "wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
 
- wf_mdecl	:: "'c wtm \\<Rightarrow> 'c wtm"
-"wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
+ wf_mdecl	:: "'c wf_mb \\<Rightarrow> 'c wf_mb"
+"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
 
-  wf_cdecl	:: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
-"wf_cdecl wtm G \\<equiv>
+  wf_cdecl	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
+"wf_cdecl wf_mb G \\<equiv>
    \\<lambda>(C,(sc,fs,ms)).
 	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
-	(\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and>  unique ms \\<and>
+	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb 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'.
                  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"
+ wf_prog	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
+"wf_prog wf_mb G \\<equiv>
+   let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
 
 end