FTBFS with Moscow ML

HOL-Theorem-Prover · May 3, 2024 · 27e4453 · 27e4453
1 parent 675fcb1
commit 27e4453
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/num/theories/cv_compute/automation/cv_memLib.sml b/src/num/theories/cv_compute/automation/cv_memLib.sml
@@ -25,6 +25,7 @@ fun cv_print_term v tm = cv_print_aux v term_to_string tm;
 fun cv_print_thm v th = cv_print_aux v thm_to_string th;
 
 (* Custom version of Lib.time *)
+local open Time; in
 fun cv_time f x =
   let val start = Time.now()
       val res = f x
@@ -33,6 +34,7 @@ fun cv_time f x =
     cv_print Verbose ("Took " ^ Time.fmt 1 (finish - start) ^ " seconds.\n");
     res
   end
+end
 
 fun indent_print_aux f verbosity prefix suffix x = let
   val m = !max_print_depth