diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/MicroJava/Comp/DefsComp.thy
--- a/src/HOL/MicroJava/Comp/DefsComp.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -5,8 +5,9 @@
 
 (* Definitions for accessing parts of methods, states etc. *)
 
-theory DefsComp = JVMExec:
-
+theory DefsComp
+imports "../JVM/JVMExec"
+begin
 
 
 constdefs