--- 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"