diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index 2af33fe319608b2d2cf7b721b6560995404028c2..1802af5fe9a7d240a7bb60eeae0533307acb4e6b 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -302,7 +302,7 @@ End
 Definition isJoin_def:
   isJoin m1 m2 mj =
     if (isFixedPoint m1 /\ isFixedPoint m2)
-    then morePrecise m1 mj /\ morePrecise m2 mj
+    then morePrecise mj m1 /\ morePrecise mj m2
     else
       (case join_fl m1 m2 of
       |NONE => F
@@ -312,7 +312,7 @@ End
 Definition isJoin3_def:
   isJoin3 m1 m2 m3 mj =
     if (isFixedPoint m1 /\ isFixedPoint m2 /\ isFixedPoint m3)
-    then morePrecise m1 mj /\ morePrecise m2 mj /\ morePrecise m3 mj
+    then morePrecise mj m1 /\ morePrecise mj m2 /\ morePrecise mj m3
     else
       (case join_fl3 m1 m2 m3 of
        |NONE => F
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 4e6676a30108e16321bd4a434f8045f9f076faa5..38cc3482cd370d92d70591d0983b10ce035bc9a8 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -131,7 +131,7 @@ Definition getValidMap_def:
           case mOldO of
           | NONE => Fail "Undefined fixed-point type"
           | SOME mj =>
-            if (morePrecise t1 mj /\ morePrecise t2 mj)
+            if (morePrecise mj t1 /\ morePrecise mj t2)
             then addMono e mj akk2_map
             else Fail "Incorrect fixed-point type"
         else
@@ -165,7 +165,7 @@ Definition getValidMap_def:
           case mOldO of
           | NONE => Fail "Undefined fixed-point type"
           | SOME mj =>
-            if (morePrecise t1 mj /\ morePrecise t2 mj /\ morePrecise t3 mj)
+            if (morePrecise mj t1 /\ morePrecise mj t2 /\ morePrecise mj t3)
             then addMono e mj akk3_map
             else Fail "Incorrect fixed-point type"
         else if (t1 = REAL ∨ t2 = REAL ∨ t3 = REAL)
@@ -254,7 +254,7 @@ Proof
       \\ Cases_on `getValidMap Gamma e1 akk` \\ fs[result_bind_def]
       \\ Cases_on `getValidMap Gamma e2 a` \\ fs[option_case_eq]
       \\ Cases_on `isFixedPoint t1` \\ Cases_on `isFixedPoint t2` \\ fs[option_case_eq]
-      >- (Cases_on `morePrecise t1 mj` \\ Cases_on `morePrecise t2 mj`
+      >- (Cases_on `morePrecise mj t1` \\ Cases_on `morePrecise mj t2`
           \\ fs[addMono_def, option_case_eq]
           \\ rveq \\ res_tac
           \\ by_monotonicity)
@@ -277,9 +277,9 @@ Proof
       \\ Cases_on `isFixedPoint t2`
       \\ Cases_on `isFixedPoint t3`
       \\ fs[option_case_eq]
-      >- (Cases_on `morePrecise t1 mj`
-          \\ Cases_on `morePrecise t2 mj`
-          \\ Cases_on `morePrecise t3 mj`
+      >- (Cases_on `morePrecise mj t1`
+          \\ Cases_on `morePrecise mj t2`
+          \\ Cases_on `morePrecise mj t3`
           \\ fs[addMono_def, option_case_eq]
           \\ rveq \\ res_tac
           \\ by_monotonicity)
@@ -475,7 +475,7 @@ Proof
         by (rpt strip_tac \\ first_x_assum irule \\ fs[]
             \\ qexistsl_tac [`Gamma`, `a`] \\ fs[])
       \\ Cases_on ‘isFixedPoint x ∧ isFixedPoint x'’
-      >- (fs[option_case_eq] \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
+      >- (fs[option_case_eq] \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
           \\ fs[addMono_def, option_case_eq]
           \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
           \\ reverse (Cases_on `e'' = Binop b e1 e2`) \\ fs[]
@@ -604,8 +604,8 @@ Proof
             \\ qexistsl_tac [`Gamma`, `map2`] \\ fs[])
       \\ Cases_on `isFixedPoint x /\ isFixedPoint x' /\ isFixedPoint x''`
       >- (fs[option_case_eq]
-          \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
-          \\ Cases_on `morePrecise x'' mj`
+          \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
+          \\ Cases_on `morePrecise mj x''`
           \\ fs[addMono_def, option_case_eq]
           \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
           \\ rename1 `if eNew = Fma e1 e2 e3 then SOME mj else _`