diff -r 3a0c996cf2b2 -r b7f7e18eb584 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Mon Dec 06 14:23:45 1999 +0100
@@ -188,10 +188,10 @@
 
 
  wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
- "wt_method G cn pTs rT mxl ins phi \\<equiv>
+ "wt_method G C pTs rT mxl ins phi \\<equiv>
 	let max_pc = length ins
         in
-	0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> 
+	0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> 
 	(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
 
  wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"