diff --git a/spec/Makefile b/spec/Makefile
index 5b6af1508..a79ba4907 100644
--- a/spec/Makefile
+++ b/spec/Makefile
@@ -36,7 +36,7 @@ spec-check: .FORCE
 
 # Preprocess the kernel's source code and bitfield theory files.
 c-kernel: .FORCE
-	cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) -B kernel_all.c_pp theories
+	cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec
 .PHONY: c-kernel
 
 # Produce the input data for the binary verification problem at -O1
@@ -50,5 +50,6 @@ clean:
 	rm -rf abstract/generated
 	cd cspec/c && $(MAKE) clean SKIP_PATH_CHECKS=1
 	rm -f umm_types.txt
+.PHONY: clean
 
 include ../misc/isa-common.mk
diff --git a/spec/cspec/c/Makefile b/spec/cspec/c/Makefile
index 709de5daa..ddc1003d1 100644
--- a/spec/cspec/c/Makefile
+++ b/spec/cspec/c/Makefile
@@ -33,9 +33,10 @@ FASTPATH=yes
 CSPEC_DIR=..
 CONFIG_DOMAIN_SCHEDULE=config.c
 
-.PHONY: newdefault
-
-newdefault: kernel_all.c_pp theories
+# called by ../../spec/Makefile
+cspec: kernel_all.c_pp ${UMM_TYPES} theories
+# theories is defined in seL4 makefile
+.PHONY: cspec
 
 # Create "umm_types" if necessary.
 ${UMM_TYPES}: kernel_all.c_pp