--- a/src/HOL/MicroJava/BV/Correct.thy Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Wed Jan 12 15:58:16 2000 +0100
@@ -13,8 +13,7 @@
"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
-"approx_loc G hp loc LT \\<equiv>
- length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)"
+"approx_loc G hp loc LT \\<equiv> list_all2 (approx_val G hp) loc LT"
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)"