src/Pure/General/value.ML

--- a/src/Pure/General/value.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/General/value.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -13,8 +13,6 @@
   val print_int: int -> string
   val parse_real: string -> real
   val print_real: real -> string
-  val parse_time: string -> Time.time
-  val print_time: Time.time -> string
 end;
 
 structure Value: VALUE =
@@ -82,16 +80,4 @@
     | _ => s)
   end;
 
-
-(* time *)
-
-fun parse_time s =
-  (case Time.fromString s of
-    SOME x => x
-  | NONE => raise Fail ("Bad time " ^ quote s));
-
-fun print_time x =
-  if x < Time.zeroTime then "-" ^ Time.toString (Time.zeroTime - x)
-  else Time.toString x;
-
 end;