diff -r 2950128b8206 -r f4c64597fb02 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Oct 23 16:10:02 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Wed Oct 23 16:10:42 2002 +0200
@@ -33,45 +33,15 @@
 section {* Exceptions *}
 constdefs
   raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
-  "raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None"
-
-  -- "redefines State.new\\_Addr:"
-  new_Addr :: "aheap \<Rightarrow> loc \<times> val option"
-  "new_Addr h \<equiv> let (a, x) = State.new_Addr h 
-                in  (a, raise_system_xcpt (x ~= None) OutOfMemory)"
-
+  "raise_system_xcpt b x \<equiv> raise_if b x None"
 
 section {* Runtime State *}
 types
   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
-text {* a new, blank object with default values in all fields: *}
-constdefs
-  blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
-  "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
-
-  start_heap :: "'c prog \<Rightarrow> aheap"
-  "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
-                        (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
-                        (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
-
 section {* Lemmas *}
 
-lemma new_AddrD:
-  assumes new: "new_Addr hp = (ref, xcp)" 
-  shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
-proof -
-  from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)"
-    by (cases "State.new_Addr hp") (simp add: new_Addr_def)
-  from this [symmetric] 
-  have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory" 
-    by (rule State.new_AddrD)
-  with new old show ?thesis
-    by (auto simp add: new_Addr_def raise_system_xcpt_def)
-qed
-
-
 lemma new_Addr_OutOfMemory:
   "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
 proof - 
@@ -82,4 +52,4 @@
   show ?thesis by (auto dest: new_AddrD)
 qed
   
-end
\ No newline at end of file
+end