diff --git a/Multivariate/canal.ml b/Multivariate/canal.ml
index ef5cc02d..be30c21d 100644
--- a/Multivariate/canal.ml
+++ b/Multivariate/canal.ml
@@ -2391,7 +2391,7 @@ let HOLOMORPHIC_CONSTANT_IM = prove
 (* Differentiation conversion.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-let complex_differentiation_theorems = ref [];;
+let complex_differentiation_theorems = ref ([]: thm list);;
 
 let add_complex_differentiation_theorems =
   let ETA_THM = prove
diff --git a/Multivariate/clifford.ml b/Multivariate/clifford.ml
index 8da82a7f..3664d52d 100644
--- a/Multivariate/clifford.ml
+++ b/Multivariate/clifford.ml
@@ -761,7 +761,7 @@ let SETENUM_NORM_CONV =
     GEN_REWRITE_CONV I [FORALL_SIMP] in
   fun tm ->
     let nums = dest_setenum tm in
-    let nums' = map mk_numeral (sort (</) (map dest_numeral (setify nums))) in
+    let nums' = map mk_numeral (sort (</) (map dest_numeral (setify Term.(<) nums))) in
     if nums' = nums then REFL tm else
     let eq = mk_eq(tm,mk_setenum(nums',fst(dest_fun_ty(type_of tm)))) in
     EQT_ELIM(conv eq);;
@@ -829,7 +829,7 @@ let MBASIS_GROUP_CONV tm =
   let vadd_tm = rator(rator tm) in
   let mk_vadd = mk_binop vadd_tm in
   let mbs = map (snd o dest_binary "%") tms in
-  let tmbs = zip mbs tms and mset = setify mbs in
+  let tmbs = zip mbs tms and mset = setify Term.(<) mbs in
   let grps = map (fun x -> map snd (filter (fun (x',_) -> x' = x) tmbs))
                  mset in
   let tm' = end_itlist mk_vadd (map (end_itlist mk_vadd) grps) in
diff --git a/Multivariate/realanalysis.ml b/Multivariate/realanalysis.ml
index 766daae6..ee6eddcb 100644
--- a/Multivariate/realanalysis.ml
+++ b/Multivariate/realanalysis.ml
@@ -4326,7 +4326,7 @@ let REAL_CONTINUOUS_ON_ACS = prove
 (* Differentiation conversion.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-let real_differentiation_theorems = ref [];;
+let real_differentiation_theorems = ref ([]: thm list);;
 
 let add_real_differentiation_theorems =
   let ETA_THM = prove
diff --git a/build-instructions.sh b/build-instructions.sh
index cc071efc..ade35db3 100755
--- a/build-instructions.sh
+++ b/build-instructions.sh
@@ -12,7 +12,8 @@ tar xvzf cake-x64-64.tar.gz --strip-components=1
 
 # By default, the CakeML compiler reserves a few kilobytes for constants and
 # code produced by the dynamic compiler. Using Candle requires setting these
-# to some megabytes:
+# to some megabytes (or hundreds of megabytes for some of the more heavier
+# files in HOL Light, such as make_complex.ml).
 patch cake.S ../cake.S.patch
 
 # Patching in useful FFI calls
diff --git a/candle/cake.S.patch b/candle/cake.S.patch
index ba2e9cde..d0fe686a 100644
--- a/candle/cake.S.patch
+++ b/candle/cake.S.patch
@@ -2,5 +2,5 @@
 < #define DATA_BUFFER_SIZE    65536
 < #define CODE_BUFFER_SIZE  5242880
 ---
-> #define DATA_BUFFER_SIZE  65536000
-> #define CODE_BUFFER_SIZE  52428800
+> #define DATA_BUFFER_SIZE  655360000
+> #define CODE_BUFFER_SIZE  524288000