--- a/src/HOL/Code_Eval.thy Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Code_Eval.thy Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Eval
-imports Plain RType
+imports Plain "~~/src/HOL/Library/RType"
begin
subsection {* Term representation *}
--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
header{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
-imports Univ_Poly Dense_Linear_Order Complex
+imports "~~/src/HOL/Library/Univ_Poly" "~~/src/HOL/Library/Dense_Linear_Order" Complex
begin
subsection {* Square root of complex numbers *}
--- a/src/HOL/Real/Rational.thy Mon Sep 22 13:55:59 2008 +0200
+++ b/src/HOL/Real/Rational.thy Mon Sep 22 13:56:01 2008 +0200
@@ -6,7 +6,7 @@
header {* Rational numbers *}
theory Rational
-imports "../Nat_Int_Bij" GCD
+imports "../Nat_Int_Bij" "~~/src/HOL/Library/GCD"
uses ("rat_arith.ML")
begin