# HG changeset patch
# User kleing
# Date 1011133389 -3600
# Node ID 501da8288f05295e37698840d53096a776b7f565
# Parent  a47f51daa6dc9567626211eade21074f23266b11
fixed theory deps

diff -r a47f51daa6dc -r 501da8288f05 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Tue Jan 15 22:22:05 2002 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Jan 15 23:23:09 2002 +0100
@@ -9,7 +9,7 @@
 
 header "BV Type Safety Invariant"
 
-theory Correct = BVSpec:
+theory Correct = BVSpec + JVMExec:
 
 constdefs
   approx_val :: "[jvm_prog,aheap,val,ty err] => bool"