diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -6,7 +6,10 @@
 
 header {* \isaheader{Effect of Instructions on the State Type} *}
 
-theory Effect = JVMType + JVMExceptions:
+theory Effect 
+imports JVMType "../JVM/JVMExceptions"
+begin
+
 
 types
   succ_type = "(p_count \<times> state_type option) list"