--- a/src/HOL/MicroJava/BV/JVM.thy Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Nov 24 14:37:23 2009 +0100
@@ -5,8 +5,9 @@
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
-theory JVM imports Kildall Typing_Framework_JVM begin
-
+theory JVM
+imports Typing_Framework_JVM
+begin
constdefs
kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow>
@@ -39,7 +40,7 @@
simp add: symmetric sl_triple_conv)
apply (simp (no_asm) add: JVM_le_unfold)
apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
- dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
+ dest: wf_subcls1 wf_acyclic wf_prog_ws_prog)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
apply assumption