diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -30,14 +30,12 @@
 
  wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
 "wf_cdecl wf_mb G ==
-   \\<lambda>(C,(sc,fs,ms)).
-  (\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
+   \\<lambda>(C,(D,fs,ms)).
+  (\\<forall>f\\<in>set fs. wf_fdecl G         f) \\<and>  unique fs \\<and>
   (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
-  (case sc of None => C = Object
-         | Some D =>
-             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
-             (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
-                 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
+  (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and>  \\<not>G\\<turnstile>D\\<preceq>C C \\<and>
+                   (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
+                      method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
 
  wf_prog :: "'c wf_mb => 'c prog => bool"
 "wf_prog wf_mb G ==