diff --git a/examples/HolBdd/MachineTransitionScript.sml b/examples/HolBdd/MachineTransitionScript.sml
index 59241f352a..ebf59ab17d 100644
--- a/examples/HolBdd/MachineTransitionScript.sml
+++ b/examples/HolBdd/MachineTransitionScript.sml
@@ -990,6 +990,7 @@ val TotalMooreTrans =
     THEN Q.EXISTS_TAC `(q',nextfn(q,r))`
     THEN RW_TAC std_ss [MooreTrans_def]);
 
+(* NOTE: duplicated with the next theorem but let's keep the original code:
 val ReachableMooreTrans =
  save_thm
   ("ReachableMooreTrans",
@@ -997,6 +998,7 @@ val ReachableMooreTrans =
     [``\(input:'a,state:'b). (input = inputs 0) /\ (state = states 0)``,
      ``(input:'a, state:'b)``]
     (MATCH_MP ReachablePath TotalMooreTrans));
+ *)
 
 (*****************************************************************************)
 (*   val ReachableMooreTrans =                                               *)
diff --git a/examples/temporal_deep/src/model_check/selftest.sml b/examples/temporal_deep/src/model_check/selftest.sml
index 1ec1c9c5b8..a27e295c0c 100644
--- a/examples/temporal_deep/src/model_check/selftest.sml
+++ b/examples/temporal_deep/src/model_check/selftest.sml
@@ -25,7 +25,7 @@ fun modelCheck_test1 () = let
 in
   if aconv (concl (valOf test1)) result1 then OK ()
   else die ("Got " ^ term_to_string (concl (valOf test1)));
-  Process.system ("rm " ^ (!model_check_temp_file)))
+  Process.system ("rm " ^ (!model_check_temp_file))
 end;
 
 fun modelCheck_test2 () = let
@@ -34,7 +34,7 @@ in
   if (isSome test2) then
     die ("Got " ^ term_to_string (concl (valOf test2)))
   else OK ();
-  Process.system ("rm " ^ (!model_check_temp_file)))
+  Process.system ("rm " ^ (!model_check_temp_file))
 end;
 
 val _ = modelCheck_test1 ();