src/HOL/SMT/SMT_Base.thy

--- a/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 00:45:02 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Thu Feb 11 09:14:08 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")