# HG changeset patch
# User kleing
# Date 1035454113 -7200
# Node ID c748d11547d82301ba15da0a53719591074a5641
# Parent  5fad004bd9dfa943f65ed5325833f1849faec440
changes for cleanup in JVM

diff -r 5fad004bd9df -r c748d11547d8 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Oct 24 12:07:31 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Oct 24 12:08:33 2002 +0200
@@ -281,7 +281,7 @@
       by (clarsimp simp add: app_def)
 
     with eff stk loc pc'
-    have "check_instr (ins!pc) G hp stk loc C sig pc (length ins) frs'"
+    have "check_instr (ins!pc) G hp stk loc C sig pc frs'"
     proof (cases "ins!pc")
       case (Getfield F C) 
       with app stk loc phi obtain v vT stk' where
diff -r 5fad004bd9df -r c748d11547d8 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Oct 24 12:07:31 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Oct 24 12:08:33 2002 +0200
@@ -668,7 +668,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def 
+apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def split_beta
                 split: option.split split_if_asm)
 apply (frule conf_widen)
 apply assumption+