diff --git a/examples/dependability/RBD/Holmakefile b/examples/dependability/RBD/Holmakefile
index 443c1038eb..2ea674ca1c 100644
--- a/examples/dependability/RBD/Holmakefile
+++ b/examples/dependability/RBD/Holmakefile
@@ -1,2 +1,2 @@
-INCDIRS = examples/miller/formalize src/probability src/real/analysis
+INCDIRS = examples/miller/formalize src/probability examples/probability/legacy src/real/analysis
 INCLUDES = $(patsubst %,$(dprot $(HOLDIR)/%),$(INCDIRS))
diff --git a/examples/diningcryptos/Holmakefile b/examples/diningcryptos/Holmakefile
index 8786248ddd..c7a8e5bbb0 100644
--- a/examples/diningcryptos/Holmakefile
+++ b/examples/diningcryptos/Holmakefile
@@ -1,2 +1,2 @@
-INCLUDES = ../miller/subtypes ../miller/formalize $(HOLDIR)/src/probability \
+INCLUDES = ../miller/subtypes ../miller/formalize $(HOLDIR)/examples/probability/legacy \
 	$(HOLDIR)/src/real/analysis
diff --git a/examples/miller/prob/Holmakefile b/examples/miller/prob/Holmakefile
index 532721efc9..279d824c50 100644
--- a/examples/miller/prob/Holmakefile
+++ b/examples/miller/prob/Holmakefile
@@ -1,2 +1,2 @@
 INCLUDES = ../formalize ../ho_prover ../subtypes ../../Crypto/RSA \
-	   $(HOLDIR)/src/real $(HOLDIR)/src/probability
+	   $(HOLDIR)/src/real $(HOLDIR)/examples/probability/legacy
diff --git a/examples/probability/legacy/Holmakefile b/examples/probability/legacy/Holmakefile
new file mode 100644
index 0000000000..160cfb5e18
--- /dev/null
+++ b/examples/probability/legacy/Holmakefile
@@ -0,0 +1,8 @@
+INCLUDES = $(HOLDIR)/src/real $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/analysis \
+	$(HOLDIR)/src/probability
+
+EXTRA_CLEANS = $(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
+
+all: $(DEFAULT_TARGETS)
+
+.PHONY: all
diff --git a/examples/probability/legacy/README.md b/examples/probability/legacy/README.md
new file mode 100644
index 0000000000..3b0793c6a5
--- /dev/null
+++ b/examples/probability/legacy/README.md
@@ -0,0 +1,7 @@
+# HOL's Legacy Probability Theory based on Finite Measure Theory
+
+The following theories in this directory was in `$(HOLDIR)/src/probability`:
+
+     real_measureScript.sml       * Finite Measure Theory (based on reals)
+     real_lebesgueScript.sml      * Lebesgue Integration based on Finite Measures
+     real_probabilityScript.sml   * Probability Theory based on Finite Measures
diff --git a/src/probability/real_lebesgueScript.sml b/examples/probability/legacy/real_lebesgueScript.sml
similarity index 100%
rename from src/probability/real_lebesgueScript.sml
rename to examples/probability/legacy/real_lebesgueScript.sml
diff --git a/src/probability/real_measureScript.sml b/examples/probability/legacy/real_measureScript.sml
similarity index 100%
rename from src/probability/real_measureScript.sml
rename to examples/probability/legacy/real_measureScript.sml
diff --git a/src/probability/real_probabilityScript.sml b/examples/probability/legacy/real_probabilityScript.sml
similarity index 100%
rename from src/probability/real_probabilityScript.sml
rename to examples/probability/legacy/real_probabilityScript.sml
diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile
index 8dfb7d6a99..cbba1beccc 100644
--- a/src/parallel_builds/core/Holmakefile
+++ b/src/parallel_builds/core/Holmakefile
@@ -81,7 +81,7 @@ EX2DIRS = AKS algebra algorithms/boyer_moore \
             logic/ltl logic/temporal_deep \
             logic/ltl-transformations \
             l3-machine-code/decompilers \
-          miller \
+          probability/legacy miller \
           probability vector \
           separationLogic/src separationLogic/src/holfoot simple_complexity
 
diff --git a/src/probability/README.md b/src/probability/README.md
index 3f9e670d14..8242b17269 100644
--- a/src/probability/README.md
+++ b/src/probability/README.md
@@ -19,9 +19,9 @@ This directory contains HOL4's Measure, Lebesgue Integration and Probability the
 
 ## Measure, Integration and Probability Theory defined on reals (obsoleted)
 
-     real_measureScript.sml       * Measure Theory defined on reals
-     real_lebesgueScript.sml      * Lebesgue integration based on reals
-     real_probabilityScript.sml   * Probability Theory based on reals
+     NOTE: The legacy measure, integration and probability theories based on finite measures
+     are moved to `$(HOLDIR)/examples/probability/legacy`. They are needed when building the
+     two examples in `examples/miller` and `examples/diningcryptos`.
 
 ## Further extensions