src/HOL/MicroJava/J/Exceptions.thy

--- a/src/HOL/MicroJava/J/Exceptions.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
     Copyright   2002 Technische Universitaet Muenchen
 *)
 
-theory Exceptions = State:
+theory Exceptions imports State begin
 
 text {* a new, blank object with default values in all fields: *}
 constdefs