diff --git a/proof/ROOT b/proof/ROOT
index 12be36a06..9e09d3659 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -77,6 +77,8 @@ session CRefineSyscall = CBaseRefine +
     "crefine/$L4V_ARCH/Syscall_C"
 
 session CRefine = CBaseRefine +
+  theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
+    "crefine/$L4V_ARCH/Refine_C"
   theories
     "crefine/$L4V_ARCH/Refine_C"