diff -r 6a973bd43949 -r 1bc3b688548c src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Tue Nov 24 14:37:23 2009 +0100
@@ -1,13 +1,13 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
 
-theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin
-
+theory Typing_Framework_JVM
+imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
+begin
 
 constdefs
   exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state step_type"