diff --git a/lib/clib/Corres_C.thy b/lib/clib/Corres_C.thy
index b0816248b..22b35c6c9 100644
--- a/lib/clib/Corres_C.thy
+++ b/lib/clib/Corres_C.thy
@@ -11,7 +11,7 @@
 theory Corres_C
 imports 
 	CCorresLemmas 
-	"../../proof/crefine/SR_lemmas_C"
+	"../../proof/crefine/$L4V_ARCH/SR_lemmas_C"
 begin
 
 abbreviation
diff --git a/proof/ROOT b/proof/ROOT
index 2a48843a4..d42675bfe 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -56,17 +56,17 @@ session AInvs = ASpec +
 
 session CRefineSyscall = CBaseRefine +
   theories
-    "crefine/Syscall_C"
+    "crefine/$L4V_ARCH/Syscall_C"
 
 session CRefine = CBaseRefine +
   theories
-    "crefine/Refine_C"
+    "crefine/$L4V_ARCH/Refine_C"
 
 session CBaseRefine = CSpec +
   theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
-    "crefine/Include_C"
+    "crefine/$L4V_ARCH/Include_C"
   theories
-    "crefine/Include_C"
+    "crefine/$L4V_ARCH/Include_C"
 
 
 (*
diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy
index 79f4aa6d8..f86915ce1 100644
--- a/proof/crefine/ARM/ADT_C.thy
+++ b/proof/crefine/ARM/ADT_C.thy
@@ -11,7 +11,7 @@
 theory ADT_C
 imports
   Schedule_C Retype_C Recycle_C
-  "../invariant-abstract/BCorres2_AI"
+  "../../invariant-abstract/BCorres2_AI"
 begin
 
 
diff --git a/proof/crefine/ARM/AutoCorres_C.thy b/proof/crefine/ARM/AutoCorres_C.thy
index a9192d419..4d0cfe64b 100644
--- a/proof/crefine/ARM/AutoCorres_C.thy
+++ b/proof/crefine/ARM/AutoCorres_C.thy
@@ -14,10 +14,10 @@ text \<open>
   See AutoCorresTest for example usage.
 \<close>
 theory AutoCorres_C imports
-  "../../tools/autocorres/AutoCorres"
-  "../../tools/autocorres/L4VerifiedLinks"
-  "../../lib/clib/AutoCorresModifiesProofs"
-  "../../lib/clib/Corres_C"
+  "../../../tools/autocorres/AutoCorres"
+  "../../../tools/autocorres/L4VerifiedLinks"
+  "../../../lib/clib/AutoCorresModifiesProofs"
+  "../../../lib/clib/Corres_C"
 begin
 
 context kernel begin
@@ -315,4 +315,4 @@ lemmas [terminates_trivial] =
   terminates.Skip
   terminates.Spec
 
-end
\ No newline at end of file
+end
diff --git a/proof/crefine/ARM/CLevityCatch.thy b/proof/crefine/ARM/CLevityCatch.thy
index 88628de0a..cc5f5731b 100644
--- a/proof/crefine/ARM/CLevityCatch.thy
+++ b/proof/crefine/ARM/CLevityCatch.thy
@@ -11,8 +11,8 @@
 theory CLevityCatch
 imports
   Include_C
-  "../../lib/LemmaBucket_C"
-  "../../lib/LemmaBucket"
+  "../../../lib/LemmaBucket_C"
+  "../../../lib/LemmaBucket"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/crefine/ARM/CSpaceAcc_C.thy b/proof/crefine/ARM/CSpaceAcc_C.thy
index 5348b6342..7305c9ada 100644
--- a/proof/crefine/ARM/CSpaceAcc_C.thy
+++ b/proof/crefine/ARM/CSpaceAcc_C.thy
@@ -11,7 +11,7 @@
 (* collects lemmas common to the various CSpace branches *)
 
 theory CSpaceAcc_C
-imports "../refine/$L4V_ARCH/EmptyFail" "../../lib/clib/Ctac"
+imports "../../refine/$L4V_ARCH/EmptyFail" "../../../lib/clib/Ctac"
 begin
 
 (* For resolving schematics *) 
diff --git a/proof/crefine/ARM/CSpace_RAB_C.thy b/proof/crefine/ARM/CSpace_RAB_C.thy
index d2edbd507..bb9612223 100644
--- a/proof/crefine/ARM/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM/CSpace_RAB_C.thy
@@ -9,7 +9,7 @@
  *)
 
 theory CSpace_RAB_C
-imports CSpaceAcc_C "../../lib/clib/MonadicRewrite_C"
+imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C"
 begin
 
 context kernel
diff --git a/proof/crefine/ARM/DetWP.thy b/proof/crefine/ARM/DetWP.thy
index c4b18f8dd..3ddb0050b 100644
--- a/proof/crefine/ARM/DetWP.thy
+++ b/proof/crefine/ARM/DetWP.thy
@@ -9,7 +9,7 @@
  *)
 
 theory DetWP
-imports "../../lib/clib/DetWPLib" Include_C
+imports "../../../lib/clib/DetWPLib" Include_C
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/crefine/ARM/Detype_C.thy b/proof/crefine/ARM/Detype_C.thy
index 5655e3d97..f9092a851 100644
--- a/proof/crefine/ARM/Detype_C.thy
+++ b/proof/crefine/ARM/Detype_C.thy
@@ -9,7 +9,7 @@
  *)
 
 theory Detype_C
-imports "../../lib/clib/Ctac" TcbQueue_C
+imports "../../../lib/clib/Ctac" TcbQueue_C
 begin
 
 lemma typ_clear_region_out:
diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy
index 80ca41209..7753c0139 100644
--- a/proof/crefine/ARM/Fastpath_C.thy
+++ b/proof/crefine/ARM/Fastpath_C.thy
@@ -14,8 +14,8 @@ imports
   SyscallArgs_C
   Delete_C
   Syscall_C
-  "../refine/$L4V_ARCH/RAB_FN"
-  "../../lib/clib/MonadicRewrite_C"
+  "../../refine/$L4V_ARCH/RAB_FN"
+  "../../../lib/clib/MonadicRewrite_C"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/crefine/ARM/Include_C.thy b/proof/crefine/ARM/Include_C.thy
index 52442cc79..13a076c02 100644
--- a/proof/crefine/ARM/Include_C.thy
+++ b/proof/crefine/ARM/Include_C.thy
@@ -10,8 +10,8 @@
 
 theory Include_C
 imports
-  "../../spec/cspec/KernelInc_C"
-  "../refine/$L4V_ARCH/Refine"
+  "../../../spec/cspec/$L4V_ARCH/KernelInc_C"
+  "../../refine/$L4V_ARCH/Refine"
 begin
 
 end
diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy
index 409e28e62..8c0cf310e 100644
--- a/proof/crefine/ARM/Invoke_C.thy
+++ b/proof/crefine/ARM/Invoke_C.thy
@@ -9,7 +9,7 @@
  *)
 
 theory Invoke_C
-imports Recycle_C "../../lib/clib/MonadicRewrite_C"
+imports Recycle_C "../../../lib/clib/MonadicRewrite_C"
 begin
 
 context kernel_m
diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy
index 184c774cb..6c9778ff2 100644
--- a/proof/crefine/ARM/IsolatedThreadAction.thy
+++ b/proof/crefine/ARM/IsolatedThreadAction.thy
@@ -9,7 +9,7 @@
  *)
 
 theory IsolatedThreadAction
-imports "../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
+imports "../../../lib/clib/MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
 begin
 
 datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
diff --git a/proof/crefine/ARM/Machine_C.thy b/proof/crefine/ARM/Machine_C.thy
index 2ca77ae50..8eabfc1a2 100644
--- a/proof/crefine/ARM/Machine_C.thy
+++ b/proof/crefine/ARM/Machine_C.thy
@@ -15,7 +15,7 @@
 *)
 
 theory Machine_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin
 
 locale kernel_m = kernel +
diff --git a/proof/crefine/ARM/Move.thy b/proof/crefine/ARM/Move.thy
index dc702509d..52d97e705 100644
--- a/proof/crefine/ARM/Move.thy
+++ b/proof/crefine/ARM/Move.thy
@@ -11,7 +11,7 @@
 (* things that should be moved into first refinement *)
 
 theory Move
-imports "../refine/$L4V_ARCH/Refine"
+imports "../../refine/$L4V_ARCH/Refine"
 begin
 
 lemma finaliseCap_Reply:
diff --git a/proof/crefine/ARM/PSpace_C.thy b/proof/crefine/ARM/PSpace_C.thy
index 02622c0b9..3e6e27496 100644
--- a/proof/crefine/ARM/PSpace_C.thy
+++ b/proof/crefine/ARM/PSpace_C.thy
@@ -9,7 +9,7 @@
  *)
 
 theory PSpace_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin
 
 context kernel begin
diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy
index 925dad800..d6a0a4040 100644
--- a/proof/crefine/ARM/Refine_C.thy
+++ b/proof/crefine/ARM/Refine_C.thy
@@ -11,7 +11,7 @@
 chapter "Toplevel Refinement Statement"
 
 theory Refine_C
-imports Init_C Fastpath_C "../../lib/clib/CToCRefine"
+imports Init_C Fastpath_C "../../../lib/clib/CToCRefine"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/crefine/ARM/Refine_nondet_C.thy b/proof/crefine/ARM/Refine_nondet_C.thy
index cd3ecb411..65c9ffb6b 100644
--- a/proof/crefine/ARM/Refine_nondet_C.thy
+++ b/proof/crefine/ARM/Refine_nondet_C.thy
@@ -13,7 +13,7 @@ header "Toplevel Refinement Statement for nondeterministic specification"
 theory Refine_nondet_C (* FIXME: broken *)
 imports
   Refine_C
-  "../invariant-abstract/BCorres2_AI"
+  "../../invariant-abstract/BCorres2_AI"
 begin
 
 definition (in state_rel)
diff --git a/proof/crefine/ARM/SR_lemmas_C.thy b/proof/crefine/ARM/SR_lemmas_C.thy
index 8d43594ec..4fcd8c6c7 100644
--- a/proof/crefine/ARM/SR_lemmas_C.thy
+++ b/proof/crefine/ARM/SR_lemmas_C.thy
@@ -11,7 +11,7 @@
 theory SR_lemmas_C
 imports
   StateRelation_C
-  "../refine/$L4V_ARCH/Invariants_H"
+  "../../refine/$L4V_ARCH/Invariants_H"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/crefine/ARM/TcbAcc_C.thy b/proof/crefine/ARM/TcbAcc_C.thy
index cabd1e8a5..36e6b67e2 100644
--- a/proof/crefine/ARM/TcbAcc_C.thy
+++ b/proof/crefine/ARM/TcbAcc_C.thy
@@ -9,7 +9,7 @@
  *)
 
 theory TcbAcc_C
-imports "../../lib/clib/Ctac"
+imports "../../../lib/clib/Ctac"
 begin
 
 context kernel
diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy
index 0a319709c..ed6ebb103 100644
--- a/proof/crefine/ARM/Wellformed_C.thy
+++ b/proof/crefine/ARM/Wellformed_C.thy
@@ -13,9 +13,9 @@
 
 theory Wellformed_C
 imports
-  "../../lib/CTranslationNICTA"
+  "../../../lib/CTranslationNICTA"
   CLevityCatch
-  "../../spec/cspec/Substitute"
+  "../../../spec/cspec/Substitute"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/proof/infoflow/ADT_IF_Refine_C.thy b/proof/infoflow/ADT_IF_Refine_C.thy
index 76fd9dcb9..7f1b6fd57 100644
--- a/proof/infoflow/ADT_IF_Refine_C.thy
+++ b/proof/infoflow/ADT_IF_Refine_C.thy
@@ -10,7 +10,7 @@
 
 theory ADT_IF_Refine_C
 imports    
-    "ADT_IF_Refine" "../crefine/Refine_C"
+    "ADT_IF_Refine" "../crefine/$L4V_ARCH/Refine_C"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
diff --git a/tools/autocorres/TestSEL4.thy b/tools/autocorres/TestSEL4.thy
index 8bb1c2cb5..b02b4af3b 100644
--- a/tools/autocorres/TestSEL4.thy
+++ b/tools/autocorres/TestSEL4.thy
@@ -11,7 +11,7 @@
 theory TestSEL4
 imports
   AutoCorres
-  "../../spec/cspec/KernelInc_C"
+  "../../spec/cspec/$L4V_ARCH/KernelInc_C"
 begin
 
 (*