diff --git a/Innsbruck/Demo.thy b/Innsbruck/Demo.thy
index addab064..c1840727 100644
--- a/Innsbruck/Demo.thy
+++ b/Innsbruck/Demo.thy
@@ -3,7 +3,7 @@
                 The definitions of sep and itrev are from Isabelle's tutorial.
 *)
 theory Demo
-  imports Main "../PSL/PSL" "../PaMpeR/PaMpeR" "../PSL/PSL"
+  imports "Smart_Isabelle.Smart_Isabelle" Main
 begin
 
 (*** Part I ***)
diff --git a/LiFtEr/LiFtEr.thy b/LiFtEr/LiFtEr.thy
index 47617db9..b2eea243 100644
--- a/LiFtEr/LiFtEr.thy
+++ b/LiFtEr/LiFtEr.thy
@@ -5,7 +5,7 @@ MeLoId: Machine Learning Induction for Isabelle/HOL, and
 LiFtEr: Logical Feature Extractor.
 *)
 theory LiFtEr
-  imports "SeLFiE.SeLFiE"
+  imports "SeLFiE.SeLFiE" Main
   keywords "assert_LiFtEr_true" :: diag
    and     "assert_LiFtEr_false":: diag
    and     "assert_LiFtEr"      :: diag
diff --git a/PSL/Try_Hard.thy b/PSL/Try_Hard.thy
index 0129c75d..f8582464 100644
--- a/PSL/Try_Hard.thy
+++ b/PSL/Try_Hard.thy
@@ -5,7 +5,7 @@ This file defines the default strategy "TryHard".
 *)
 
 theory Try_Hard
-imports "SeLFiE.SeLFiE"
+imports "SeLFiE.SeLFiE" Main
 keywords "strategy"     :: thy_decl
      and "find_proof"   :: diag
      and "try_hard"     :: diag
diff --git a/SeLFiE/Test_SeLFiE.thy b/SeLFiE/Test_SeLFiE.thy
index c474495e..404e1085 100644
--- a/SeLFiE/Test_SeLFiE.thy
+++ b/SeLFiE/Test_SeLFiE.thy
@@ -1,5 +1,5 @@
 theory Test_SeLFiE
-imports SeLFiE
+imports Main SeLFiE
 begin
 
 lemma "f x \<Longrightarrow> g y \<Longrightarrow> h z"