diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -52,7 +52,7 @@
 	 in
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and>
-	 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
+	 (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
                        ST = oT # ST' \\<and> 
 		       G \\<turnstile> oT \\<preceq> (Class C) \\<and>
 		       G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
@@ -63,7 +63,7 @@
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and> 
 	 (\\<exists>T vT oT ST'.
-             cfield (G,C) F = Some(C,T) \\<and>
+             field (G,C) F = Some(C,T) \\<and>
              ST = vT # oT # ST' \\<and> 
              G \\<turnstile> oT \\<preceq> (Class C) \\<and>
 	     G \\<turnstile> vT \\<preceq> T  \\<and>
@@ -155,7 +155,7 @@
          (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
          length apTs = length fpTs \\<and>
          (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
-         (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
+         (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
          G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
 
 consts