--- a/src/HOL/Analysis/Inner_Product.thy Wed Apr 19 16:25:26 2017 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Wed Apr 19 16:26:09 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Inner Product Spaces and the Gradient Derivative\<close>
theory Inner_Product
-imports "~~/src/HOL/Complex_Main"
+imports Complex_Main
begin
subsection \<open>Real inner product spaces\<close>
--- a/src/HOL/Library/Old_Datatype.thy Wed Apr 19 16:25:26 2017 +0200
+++ b/src/HOL/Library/Old_Datatype.thy Wed Apr 19 16:26:09 2017 +0200
@@ -6,7 +6,7 @@
section \<open>Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums\<close>
theory Old_Datatype
-imports "../Main"
+imports Main
keywords "old_datatype" :: thy_decl
begin