diff --git a/examples/fermat/twosq/helperTwosqScript.sml b/examples/fermat/twosq/helperTwosqScript.sml
index 3630a5c6b1..3329996c5e 100644
--- a/examples/fermat/twosq/helperTwosqScript.sml
+++ b/examples/fermat/twosq/helperTwosqScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "helperTwosq";
 
 
 (* open dependent theories *)
-val _ = load("helperFunctionTheory");
 open helperFunctionTheory;
 open helperSetTheory;
 open helperNumTheory;
@@ -24,7 +23,6 @@ open arithmeticTheory pred_setTheory;
 open dividesTheory;
 open gcdTheory; (* for GCD_IS_GREATEST_COMMON_DIVISOR *)
 
-val _ = load("logPowerTheory");
 open logPowerTheory; (* for SQRT *)
 
 open whileTheory; (* for HOARE_SPEC_DEF *)
diff --git a/examples/fermat/twosq/hoppingScript.sml b/examples/fermat/twosq/hoppingScript.sml
index 8afc854c10..a5a1b2a177 100644
--- a/examples/fermat/twosq/hoppingScript.sml
+++ b/examples/fermat/twosq/hoppingScript.sml
@@ -30,7 +30,6 @@ open helperListTheory;
 open listRangeTheory; (* for listRangeLHI_ALL_DISTINCT *)
 open indexedListsTheory; (* for findi_EL and EL_findi *)
 
-load "sublistTheory";
 open sublistTheory;
 
 open quarityTheory;
diff --git a/examples/fermat/twosq/involuteFixScript.sml b/examples/fermat/twosq/involuteFixScript.sml
index 7e2ff34caa..50736ccfdb 100644
--- a/examples/fermat/twosq/involuteFixScript.sml
+++ b/examples/fermat/twosq/involuteFixScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "involuteFix";
 
 
 (* open dependent theories *)
-val _ = load("involuteTheory");
 open helperFunctionTheory; (* for FUNPOW_2 *)
 open helperSetTheory; (* for BIJ_ELEMENT *)
 open helperNumTheory; (* for MOD_EQ *)
diff --git a/examples/fermat/twosq/iterateComputeScript.sml b/examples/fermat/twosq/iterateComputeScript.sml
index e4845a7ff3..2a44839e18 100644
--- a/examples/fermat/twosq/iterateComputeScript.sml
+++ b/examples/fermat/twosq/iterateComputeScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "iterateCompute";
 
 
 (* open dependent theories *)
-val _ = load("iterationTheory");
 open helperFunctionTheory;
 open helperSetTheory;
 open helperNumTheory;
diff --git a/examples/fermat/twosq/iterationScript.sml b/examples/fermat/twosq/iterationScript.sml
index 6880ff76f7..4059fbff5f 100644
--- a/examples/fermat/twosq/iterationScript.sml
+++ b/examples/fermat/twosq/iterationScript.sml
@@ -14,7 +14,6 @@ val _ = new_theory "iteration";
 
 
 (* open dependent theories *)
-val _ = load("helperFunctionTheory");
 (* open helperTwosqTheory; *)
 open helperFunctionTheory;
 open helperSetTheory;