diff -r 8efb5d92cf55 -r 3bf41c474a88 src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Mar 09 20:39:19 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Mar 09 20:39:46 2002 +0100
@@ -50,17 +50,20 @@
 
 
 text {*
-  System exceptions are allocated in all heaps, 
-  and they don't carry any information other than their type: 
+  System exceptions are allocated in all heaps:
 *}
 constdefs
   preallocated :: "aheap \<Rightarrow> bool"
-  "preallocated hp \<equiv> \<forall>x. hp (XcptRef x) = Some (Xcpt x, empty)"
+  "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
 
-lemma preallocated_iff [iff]:
-  "preallocated hp \<Longrightarrow> hp (XcptRef x) = Some (Xcpt x, empty)"
+lemma preallocatedD:
+  "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
   by (unfold preallocated_def) fast
 
+lemma preallocatedE [elim?]:
+  "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
+  by (fast dest: preallocatedD)
+
 lemma cname_of_xcp:
   "raise_system_xcpt b x = Some xcp \<Longrightarrow> preallocated hp 
   \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
@@ -70,9 +73,18 @@
     by (simp add: raise_system_xcpt_def split: split_if_asm)
   moreover
   assume "preallocated hp" 
-  hence "hp (XcptRef x) = Some (Xcpt x, empty)" ..
+  then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
   ultimately
   show ?thesis by simp
 qed
 
+lemma preallocated_start:
+  "preallocated (start_heap G)"
+  apply (unfold preallocated_def)
+  apply (unfold start_heap_def)
+  apply (rule allI)
+  apply (case_tac x)
+  apply (auto simp add: blank_def)
+  done
+
 end