--- a/src/HOL/Boogie/Boogie.thy Thu Feb 11 08:44:41 2010 +0100
+++ b/src/HOL/Boogie/Boogie.thy Thu Feb 11 09:14:34 2010 +0100
@@ -5,7 +5,7 @@
header {* Integration of the Boogie program verifier *}
theory Boogie
-imports SMT
+imports "~~/src/HOL/SMT/SMT"
uses
("Tools/boogie_vcs.ML")
("Tools/boogie_loader.ML")
--- a/src/HOL/SMT/SMT_Base.thy Thu Feb 11 08:44:41 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy Thu Feb 11 09:14:34 2010 +0100
@@ -5,7 +5,8 @@
header {* SMT-specific definitions and basic tools *}
theory SMT_Base
-imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports Real "~~/src/HOL/Word/Word"
+ "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
uses
("Tools/smt_normalize.ML")
("Tools/smt_monomorph.ML")