diff -r 98f52cb93d93 -r ead84e90bfeb src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Sat Jan 06 21:31:37 2001 +0100
+++ b/src/HOL/MicroJava/BV/Step.thy	Sun Jan 07 18:43:13 2001 +0100
@@ -7,7 +7,7 @@
 header {* Effect of instructions on the state type *}
 
 
-theory Step = Convert:
+theory Step = JVMType + JVMExec:
 
 
 text "Effect of instruction on the state type:"