diff --git a/testcases/regression/Holmakefile b/testcases/regression/Holmakefile
index 1c7239562119504211576f9abd731c9cb597a534..6c6bfcf5c0c61370fdc2a923ffc1881614d1fddf 100644
--- a/testcases/regression/Holmakefile
+++ b/testcases/regression/Holmakefile
@@ -1,4 +1,4 @@
-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra ../../hol4/cakeml/misc
+INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
diff --git a/testcases/regression/certificate_AdditionSimpleScript.sml b/testcases/regression/certificate_AdditionSimpleScript.sml
index 8965ff7f740ef9a6fe162de180457d902de5252a..5e0d64ff4e2971726b6840e29798dea91755f11e 100644
--- a/testcases/regression/certificate_AdditionSimpleScript.sml
+++ b/testcases/regression/certificate_AdditionSimpleScript.sml
@@ -1,4 +1,4 @@
-open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open  FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
 open simpLib realTheory realLib RealArith;
 
 val _ = new_theory "certificate_AdditionSimple";
diff --git a/testcases/regression/certificate_DopplerScript.sml b/testcases/regression/certificate_DopplerScript.sml
index ec687ff39715597086e17d3f5c99b3c7ed12503b..27f2e7b02520442a73a31164d05d1d8f1a4d5a26 100644
--- a/testcases/regression/certificate_DopplerScript.sml
+++ b/testcases/regression/certificate_DopplerScript.sml
@@ -1,4 +1,4 @@
-open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open  FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
 open simpLib realTheory realLib RealArith;
 
 val _ = new_theory "certificate_Doppler";
diff --git a/testcases/regression/certificate_HimmilbeauScript.sml b/testcases/regression/certificate_HimmilbeauScript.sml
index 37a235cc498c8736af4a06e0a1cd31d2eb61de60..1f0054035219170b93b6abc730cfff5bbddd05b6 100644
--- a/testcases/regression/certificate_HimmilbeauScript.sml
+++ b/testcases/regression/certificate_HimmilbeauScript.sml
@@ -1,4 +1,4 @@
-open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open  FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
 open simpLib realTheory realLib RealArith;
 
 val _ = new_theory "certificate_Himmilbeau";