diff -r c78a00903e52 -r 7319d384d0d3 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Tue Dec 18 18:37:56 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy	Tue Dec 18 21:28:01 2001 +0100
@@ -27,14 +27,6 @@
       state  = "aheap \<times> locals"      -- "heap, local parameter including This"
       xstate = "xcpt option \<times> state" -- "state including exception information"
 
-
-text {*
-  System exceptions are allocated in all heaps, 
-  and they don't carry any information other than their type: *}
-axioms
-  system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)"
-
-
 syntax
   heap    :: "state => aheap"
   locals  :: "state => locals"